Decision Problems for the Verification of Real-Time Software. - Michael Emmi; Rupak Majumdar (HSCC, 2006)

Dynamic test input generation for database applications. - Michael Emmi; Rupak Majumdar; Koushik Sen (ISSTA, 2007)

Lock allocation. - Michael Emmi; Jeffrey S. Fischer; Ranjit Jhala; Rupak Majumdar (POPL, 2007)

Assembling an expressive facial animation system. - Alice Wang; Michael Emmi; Petros Faloutsos (Sandbox@SIGGRAPH, 2007)

Verifying Compensating Transactions. - Michael Emmi; Rupak Majumdar (VMCAI, 2007)

Assume-Guarantee Verification for Interface Automata. - Michael Emmi; Dimitra Giannakopoulou; Corina S. Pasareanu (FM, 2008)

Type-preserving compilation for large-scale optimizing object-oriented compilers. - Juan Chen; Chris Hawblitzel; Frances Perry; Michael Emmi; Jeremy Condit; Derrick Coetzee; Polyvios Pratikakis (PLDI, 2008)

Verifying Reference Counting Implementations. - Michael Emmi; Ranjit Jhala; Eddie Kohler; Rupak Majumdar (TACAS, 2009)

Parameterized verification of transactional memories. - Michael Emmi; Rupak Majumdar; Roman Manevich (PLDI, 2010)

Delay-bounded scheduling. - Michael Emmi; Shaz Qadeer; Zvonimir Rakamaric (POPL, 2011)

On Sequentializing Concurrent Programs. - Ahmed Bouajjani; Michael Emmi; Gennaro Parlato (SAS, 2011)

Detecting Fair Non-termination in Multithreaded Programs. - Mohamed Faouzi Atig; Ahmed Bouajjani; Michael Emmi; Akash Lal (CAV, 2012)

Finding Non-terminating Executions in Distributed Asynchronous Programs. - Michael Emmi; Akash Lal (SAS, 2012)

Asynchronous programs with prioritized task-buffers. - Michael Emmi; Akash Lal; Shaz Qadeer (SIGSOFT FSE, 2012)

Verifying Concurrent Programs against Sequential Specifications. - Ahmed Bouajjani; Michael Emmi; Constantin Enea; Jad Hamza (ESOP, 2013)

Analysis of Recursively Parallel Programs. - Ahmed Bouajjani; Michael Emmi (ACM Trans. Program. Lang. Syst., 2013)

SMACK: Decoupling Source Language Details from Verifier Implementations. - Zvonimir Rakamaric; Michael Emmi (CAV, 2014)

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

Bounded phase analysis of message-passing programs. - Ahmed Bouajjani; Michael Emmi (Int. J. Softw. Tools Technol. Transf., 2014)

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

Analysis of Asynchronous Programs with Event-Based Synchronization. - Michael Emmi; Pierre Ganty; Rupak Majumdar; Fernando Rosa-Velardo (ESOP, 2015)

Checking Correctness of Concurrent Objects: Tractable Reductions to Reachability (Invited Talk). - Ahmed Bouajjani; Michael Emmi; Constantin Enea; Jad Hamza (FSTTCS, 2015)

Monitoring refinement via symbolic reasoning. - Michael Emmi; Constantin Enea; Jad Hamza (PLDI, 2015)

Tractable Refinement Checking for Concurrent Objects. - Ahmed Bouajjani; Michael Emmi; Constantin Enea; Jad Hamza (POPL, 2015)

SMACK+Corral: A Modular Verifier - (Competition Contribution). - Arvind Haran; Montgomery Carter; Michael Emmi; Akash Lal; Shaz Qadeer; Zvonimir Rakamaric (TACAS, 2015)

SMACK software verification toolchain. - Montgomery Carter; Shaobo He; Jonathan Whitaker; Zvonimir Rakamaric; Michael Emmi (ICSE (Companion Volume), 2016)

Symbolic abstract data type inference. - Michael Emmi; Constantin Enea (POPL, 2016)

Verifying Constant-Time Implementations. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; François Dupressoir; Michael Emmi (USENIX Security Symposium, 2016)

Proving Linearizability Using Forward Simulations. - Ahmed Bouajjani; Michael Emmi; Constantin Enea; Suha Orhun Mutluergil (CAV (2), 2017)

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

Exposing Non-Atomic Methods of Concurrent Objects. - Michael Emmi; Constantin Enea (CoRR, 2017)

Monitoring Weak Consistency. - Michael Emmi; Constantin Enea (CAV (1), 2018)

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

On reducing linearizability to state reachability. - Ahmed Bouajjani; Michael Emmi; Constantin Enea; Jad Hamza (Inf. Comput., 2018)

Sound, complete, and tractable linearizability monitoring for concurrent collections. - Michael Emmi; Constantin Enea (Proc. ACM Program. Lang., 2018)

On the Complexity of Checking Consistency for Replicated Data Types. - Ranadeep Biswas; Michael Emmi; Constantin Enea (CAV (2), 2019)

Violat: Generating Tests of Observational Refinement for Concurrent Objects. - Michael Emmi; Constantin Enea (CAV (2), 2019)

Application of Trust Assessment Techniques to IoBT Systems. - Ioannis Agadakos; Gabriela F. Ciocarlie; Bogdan Copos; Michael Emmi; Jemin George; Nandi Leslie; James Michaelis (MILCOM, 2019)

Weak-consistency specification via visibility relaxation. - Michael Emmi; Constantin Enea (Proc. ACM Program. Lang., 2019)

Verifying Visibility-Based Weak Consistency. - Siddharth Krishna 001; Michael Emmi; Constantin Enea; Dejan Jovanovic (ESOP, 2020)

ct-fuzz: Fuzzing for Timing Leaks. - Shaobo He; Michael Emmi; Gabriela F. Ciocarlie (ICST, 2020)

Behavioral simulation for smart contracts. - Sidi Mohamed Beillahi; Gabriela F. Ciocarlie; Michael Emmi; Constantin Enea (PLDI, 2020)

RAPID: checking API usage for the cloud in the cloud. - Michael Emmi; Liana Hadarean; Ranjit Jhala; Lee Pike; Nicolás Rosner; Martin Schäf; Aritra Sengupta; Willem Visser (ESEC/SIGSOFT FSE, 2021)

Compositional Taint Analysis for Enforcing Security Policies at Scale. - Subarno Banerjee; Siwei Cui; Michael Emmi; Antonio Filieri; Liana Hadarean; Peixuan Li; Linghui Luo; Goran Piskachev; Nicolás Rosner; Aritra Sengupta; Omer Tripp; Jingbo Wang 006 (ESEC/SIGSOFT FSE, 2023)