HSIS: A BDD-Based Environment for Formal Verification. - Adnan Aziz; Felice Balarin; Szu-Tsung Cheng; Ramin Hojati; Timothy Kam; Sriram C. Krishnan; Rajeev K. Ranjan 001; Thomas R. Shiple; Vigyan Singhal; Serdar Tasiran; Huey-Yih Wang; Robert K. Brayton; et al. (DAC, 1994)

BDD Variable Ordering for Interacting Finite State Machines. - Adnan Aziz; Serdar Tasiran; Robert K. Brayton (DAC, 1994)

Language containment of non-deterministic omega-automata. - Serdar Tasiran; Ramin Hojati; Robert K. Brayton (CHARME, 1995)

Verifying Abstractions of Timed Systems. - Serdar Tasiran; Rajeev Alur; Robert P. Kurshan; Robert K. Brayton (CONCUR, 1996)

STARI: A Case Study in Compositional and Hierarchical Timing Verification. - Serdar Tasiran; Robert K. Brayton (CAV, 1997)

MOCHA: Modularity in Model Checking. - Rajeev Alur; Thomas A. Henzinger; Freddy Y. C. Mang; Shaz Qadeer; Sriram K. Rajamani; Serdar Tasiran (CAV, 1998)

Formal verification meets simulation (tutorial abstract). - Ellen Sentovich; David L. Dill; Serdar Tasiran (ICCAD, 1999)

A Functional Validation Technique: Biased-Random Simulation Guided by Observability-Based Coverage. - Serdar Tasiran; Farzan Fallah; David G. Chinnery; Scott J. Weber; Kurt Keutzer (ICCD, 2001)

Coverage Metrics for Functional Validation of Hardware Designs. - Serdar Tasiran; Kurt Keutzer (IEEE Des. Test Comput., 2001)

Promising Directions in Hardware Design Verification (invited). - Shaz Qadeer; Serdar Tasiran (ISQED, 2002)

An assume-guarantee rule for checking simulation. - Thomas A. Henzinger; Shaz Qadeer; Sriram K. Rajamani; Serdar Tasiran (ACM Trans. Program. Lang. Syst., 2002)

Using a formal specification and a model checker to monitor and direct simulation. - Serdar Tasiran; Yuan Yu; Brannon Batson (DAC, 2003)

Checking Cache-Coherence Protocols with TLA+. - Rajeev Joshi; Leslie Lamport; John Matthews; Serdar Tasiran; Mark R. Tuttle; Yuan Yu (Formal Methods Syst. Des., 2003)

TreeJuxtaposer: scalable tree comparison using Focus+Context with guaranteed visibility. - Tamara Munzner; François Guimbretière; Serdar Tasiran; Li Zhang 001; Yunhong Zhou (ACM Trans. Graph., 2003)

Linking Simulation with Formal Verification at a Higher Level. - Serdar Tasiran; Yuan Yu; Brannon Batson (IEEE Des. Test Comput., 2004)

Runtime Refinement Checking of Concurrent Data Structures. - Serdar Tasiran; Shaz Qadeer (RV@ETAPS, 2004)

Characterizing and Exploiting Task-Load Variability and Correlation for Energy Management in multi-core systems. - Soner Yaldiz; Alper Demir 001; Serdar Tasiran; Paolo Ienne; Yusuf Leblebici (ESTIMedia, 2005)

A Novel Test Coverage Metric for Concurrently-Accessed Software Components. - Serdar Tasiran; Tayfun Elmas; Guven Bolukbasi; M. Erkan Keremoglu (FATES, 2005)

VYRD: verifYing concurrent programs by runtime refinement-violation detection. - Tayfun Elmas; Serdar Tasiran; Shaz Qadeer (PLDI, 2005)

VyrdMC: Driving Runtime Refinement Checking with Model Checkers. - Tayfun Elmas; Serdar Tasiran (RV@CAV, 2005)

Goldilocks: Efficiently Computing the Happens-Before Relation Using Locksets. - Tayfun Elmas; Shaz Qadeer; Serdar Tasiran (FATES/RV, 2006)

A classification of concurrency bugs in java benchmarks by developer intent. - M. Erkan Keremoglu; Serdar Tasiran; Tayfun Elmas (PADTAD, 2006)

Goldilocks: a race and transaction-aware java runtime. - Tayfun Elmas; Shaz Qadeer; Serdar Tasiran (PLDI, 2007)

Rollback Atomicity. - Serdar Tasiran; Tayfun Elmas (RV, 2007)

Fast Monte Carlo Estimation of Timing Yield: Importance Sampling with Stochastic Logical Effort (ISLE) - Alp Arslan Bayrakci; Alper Demir 001; Serdar Tasiran (CoRR, 2008)

Stochastic Modeling and Optimization for Energy Management in Multicore Systems: A Video Decoding Case Study. - Soner Yaldiz; Alper Demir 001; Serdar Tasiran (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008)

Using Haptics to Convey Cause-and-Effect Relations in Climate Visualization. - Nesra Yannier; Cagatay Basdogan; Serdar Tasiran; Omer Lutfi Sen (IEEE Trans. Haptics, 2008)

Verifying Optimistic Concurrency: Prophecy Variables and Backward Reasoning. - Serdar Tasiran; Ali Sezgin; Shaz Qadeer (Design and Validation of Concurrent Systems, 2009)

An annotation assistant for interactive debugging of programs with common synchronization idioms. - Tayfun Elmas; Ali Sezgin; Serdar Tasiran; Shaz Qadeer (PADTAD, 2009)

A calculus of atomic actions. - Tayfun Elmas; Shaz Qadeer; Serdar Tasiran (POPL, 2009)

Run-Time Verification of Optimistic Concurrency. - Ali Sezgin; Serdar Tasiran; Kivanç Muslu; Shaz Qadeer (RV, 2010)

Simplifying Linearizability Proofs with Reduction and Abstraction. - Tayfun Elmas; Shaz Qadeer; Ali Sezgin; Omer Subasi; Serdar Tasiran (TACAS, 2010)

Tressa: Claiming the Future. - Ali Sezgin; Serdar Tasiran; Shaz Qadeer (VSTTE, 2010)

Goldilocks: a race-aware Java runtime. - Tayfun Elmas; Shaz Qadeer; Serdar Tasiran (Commun. ACM, 2010)

Editorial. - Oleg Sokolsky; Serdar Tasiran (J. Log. Comput., 2010)

Fast Monte Carlo Estimation of Timing Yield With Importance Sampling and Transistor-Level Circuit Simulation. - Alp Arslan Bayrakci; Alper Demir 001; Serdar Tasiran (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2010)

Location pairs: a test coverage metric for shared-memory concurrent programs. - Serdar Tasiran; M. Erkan Keremoglu; Kivanç Muslu (Empir. Softw. Eng., 2012)

Runtime verification of concurrency-specific correctness criteria. - Shaz Qadeer; Serdar Tasiran (Int. J. Softw. Tools Technol. Transf., 2012)

T-Rex: a dynamic race detection tool for C/C++ transactional memory applications. - Gokcen Kestor; Osman S. Unsal; Adrián Cristal; Serdar Tasiran (EuroSys, 2014)

Towards verifying eventually consistent applications. - Burcu Kulahcioglu Ozkan; Erdal Mutlu; Serdar Tasiran (PaPEC@EuroSys, 2014)

I Know It When I See It: Observable Races in JavaScript Applications. - Erdal Mutlu; Serdar Tasiran; Benjamin Livshits (Dyla@PLDI, 2014)

Dynamic Verification for Hybrid Concurrent Programming Models. - Erdal Mutlu; Vladimir Gajinov; Adrián Cristal; Serdar Tasiran; Osman S. Unsal (RV, 2014)

Exploiting synchronization in the analysis of shared-memory asynchronous programs. - Michael Emmi; Burcu Kulahcioglu Ozkan; Serdar Tasiran (SPIN, 2014)

Automated and Modular Refinement Reasoning for Concurrent Programs. - Chris Hawblitzel; Erez Petrank; Shaz Qadeer; Serdar Tasiran (CAV (2), 2015)

Systematic Asynchrony Bug Exploration for Android Apps. - Burcu Kulahcioglu Ozkan; Michael Emmi; Serdar Tasiran (CAV (1), 2015)

Verification Tools for Transactional Programs. - Adrián Cristal; Burcu Kulahcioglu Ozkan; Ernie Cohen; Gokcen Kestor; Ismail Kuru 001; Osman S. Unsal; Serdar Tasiran; Suha Orhun Mutluergil; Tayfun Elmas (Transactional Memory, 2015)

Detecting JavaScript races that matter. - Erdal Mutlu; Serdar Tasiran; Benjamin Livshits (ESEC/SIGSOFT FSE, 2015)

Moving Around: Lipton's Reduction for TSO - (Regular Submission). - Ali Sezgin; Serdar Tasiran (VSTTE, 2015)

TRADE: Precise Dynamic Race Detection for Scalable Transactional Memory Systems. - Gokcen Kestor; Osman S. Unsal; Adrián Cristal; Serdar Tasiran (ACM Trans. Parallel Comput., 2015)

Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency. - Ahmed Bouajjani; Michael Emmi; Constantin Enea; Burcu Kulahcioglu Ozkan; Serdar Tasiran (ESOP, 2017)

EmbedSanitizer: Runtime Race Detection Tool for 32-bit Embedded ARM. - Hassan Salehe Matar; Serdar Tasiran; Didem Unat (RV, 2017)

A solver-aided language for test input generation. - Talia Ringer; Dan Grossman; Daniel Schwartz-Narbonne; Serdar Tasiran (Proc. ACM Program. Lang., 2017)

Consistency-Aware Scheduling for Weakly Consistent Programs. - Maryam Dabaghchian; Zvonimir Rakamaric; Burcu Kulahcioglu Ozkan; Erdal Mutlu; Serdar Tasiran (ACM SIGSOFT Softw. Eng. Notes, 2017)

Reasoning About TSO Programs Using Reduction and Abstraction. - Ahmed Bouajjani; Constantin Enea; Suha Orhun Mutluergil; Serdar Tasiran (CAV (2), 2018)

Continuous Formal Verification of Amazon s2n. - Andrey Chudnov; Nathan Collins; Byron Cook; Joey Dodds; Brian Huffman; Colm MacCárthaigh; Stephen Magill; Eric Mertens; Eric Mullen; Serdar Tasiran; Aaron Tomb; Eddy Westbrook (CAV (2), 2018)

SideTrail: Verifying Time-Balancing of Cryptosystems. - Konstantinos Athanasiou; Byron Cook; Michael Emmi; Colm MacCárthaigh; Daniel Schwartz-Narbonne; Serdar Tasiran (VSTTE, 2018)

Practical Methods for Reasoning About Java 8's Functional Programming Features. - David R. Cok; Serdar Tasiran (VSTTE, 2018)

Output nondeterminism detection for programming models combining dataflow with shared memory. - Hassan Salehe Matar; Erdal Mutlu; Serdar Tasiran; Didem Unat (Parallel Comput., 2018)

A mechanized refinement proof of the Chase-Lev deque using a proof system. - Suha Orhun Mutluergil; Serdar Tasiran (Computing, 2019)

A Machine-Checked Proof of Security for AWS Key Management Service. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Matthew Campagna; Ernie Cohen; Benjamin Grégoire; Vitor Pereira 002; Bernardo Portela; Pierre-Yves Strub; Serdar Tasiran (IACR Cryptol. ePrint Arch., 2019)

Code-level model checking in the software development workflow. - Nathan Chong; Byron Cook; Konstantinos Kallas; Kareem Khazem; Felipe R. Monteiro; Daniel Schwartz-Narbonne; Serdar Tasiran; Michael Tautschnig; Mark R. Tuttle (ICSE (SEIP), 2020)

Continuous Compliance. - Martin Kellogg; Martin Schäf; Serdar Tasiran; Michael D. Ernst (ASE, 2020)

Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3. - James Bornholt; Rajeev Joshi; Vytautas Astrauskas; Brendan Cully; Bernhard Kragl; Seth Markle; Kyle Sauri; Drew Schleit; Grant Slatton; Serdar Tasiran; Jacob Van Geffen; Andrew Warfield (SOSP, 2021)

Model checking boot code from AWS data centers. - Byron Cook; Kareem Khazem; Daniel Kroening; Serdar Tasiran; Michael Tautschnig; Mark R. Tuttle (Formal Methods Syst. Des., 2021)

Code-level model checking in the software development workflow at Amazon Web Services. - Nathan Chong; Byron Cook; Jonathan Eidelman; Konstantinos Kallas; Kareem Khazem; Felipe R. Monteiro; Daniel Schwartz-Narbonne; Serdar Tasiran; Michael Tautschnig; Mark R. Tuttle (Softw. Pract. Exp., 2021)

Formally Verified Cloud-Scale Authorization. - Aleks Chakarov; Jaco Geldenhuys; Matthew Heck; Michael Hicks 001; Sam Huang; Georges-Axel Jaloyan; Anjali Joshi; K. Rustan M. Leino; Mikael Mayer; Sean McLaughlin; Akhilesh Mritunjai; Clément Pit-Claudel; et al. (ICSE, 2025)