| 2013 | PLDI | CONCURRIT: a domain specific language for reproducing concurrency bugs. | Tayfun Elmas, Jacob Burnim, George C. Necula, Koushik Sen |
| 2012 | PPoPP | NDetermin: inferring nondeterministic sequential specifications for parallelism correctness. | Jacob Burnim, Tayfun Elmas, George C. Necula, Koushik Sen |
| 2011 | PLDI | NDSeq: runtime checking for nondeterministic sequential specifications of parallel correctness. | Jacob Burnim, Tayfun Elmas, George C. Necula, Koushik Sen |
| 2010 | ICSE | QED: a proof system based on reduction and abstraction for the static verification of concurrent software. | Tayfun Elmas |
| 2010 | TACAS | Simplifying Linearizability Proofs with Reduction and Abstraction. | Tayfun Elmas, Shaz Qadeer, Ali Sezgin, Omer Subasi, Serdar Tasiran |
| 2009 | ISSTA | An annotation assistant for interactive debugging of programs with common synchronization idioms. | Tayfun Elmas, Ali Sezgin, Serdar Tasiran, Shaz Qadeer |
| 2009 | POPL | A calculus of atomic actions. | Tayfun Elmas, Shaz Qadeer, Serdar Tasiran |
| 2007 | PLDI | Goldilocks: a race and transaction-aware java runtime. | Tayfun Elmas, Shaz Qadeer, Serdar Tasiran |
| 2007 | RV | Rollback Atomicity. | Serdar Tasiran, Tayfun Elmas |
| 2006 | ISSTA | A classification of concurrency bugs in java benchmarks by developer intent. | M. Erkan Keremoglu, Serdar Tasiran, Tayfun Elmas |
| 2005 | PLDI | VYRD: verifYing concurrent programs by runtime refinement-violation detection. | Tayfun Elmas, Serdar Tasiran, Shaz Qadeer |