Michael Emmi

Publication Activity (10 Years)

Years Active: 2006-2023
Publications (10 Years): 22

Top Topics

Consistency Checking

Symbolic Reasoning

Top Venues

Publications

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
Compositional Taint Analysis for Enforcing Security Policies at Scale. ESEC/SIGSOFT FSE (2023)
Michael Emmi, Liana Hadarean, Ranjit Jhala, Lee Pike, Nicolás Rosner, Martin Schäf, Aritra Sengupta, Willem Visser
RAPID: checking API usage for the cloud in the cloud. ESEC/SIGSOFT FSE (2021)
Siddharth Krishna, Michael Emmi, Constantin Enea, Dejan Jovanovic
Verifying Visibility-Based Weak Consistency. ESOP (2020)
Sidi Mohamed Beillahi, Gabriela F. Ciocarlie, Michael Emmi, Constantin Enea
Behavioral simulation for smart contracts. PLDI (2020)
Shaobo He, Michael Emmi, Gabriela F. Ciocarlie
ct-fuzz: Fuzzing for Timing Leaks. ICST (2020)
Michael Emmi, Constantin Enea
Weak-consistency specification via visibility relaxation. Proc. ACM Program. Lang. 3 (POPL) (2019)
Shaobo He, Michael Emmi, Gabriela F. Ciocarlie
ct-fuzz: Fuzzing for Timing Leaks. CoRR (2019)
Ranadeep Biswas, Michael Emmi, Constantin Enea
On the Complexity of Checking Consistency for Replicated Data Types. CAV (2) (2019)
Siddharth Krishna, Michael Emmi, Constantin Enea, Dejan Jovanovic
Verifying Visibility-Based Weak Consistency. CoRR (2019)
Ioannis Agadakos, Gabriela F. Ciocarlie, Bogdan Copos, Michael Emmi, Jemin George, Nandi Leslie, James Michaelis
Application of Trust Assessment Techniques to IoBT Systems. MILCOM (2019)
Michael Emmi, Constantin Enea
Violat: Generating Tests of Observational Refinement for Concurrent Objects. CAV (2) (2019)
Konstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCárthaigh, Daniel Schwartz-Narbonne, Serdar Tasiran
SideTrail: Verifying Time-Balancing of Cryptosystems. VSTTE (2018)
Michael Emmi, Constantin Enea
Monitoring Weak Consistency. CAV (1) (2018)
Michael Emmi, Constantin Enea
Sound, complete, and tractable linearizability monitoring for concurrent collections. Proc. ACM Program. Lang. 2 (POPL) (2018)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
On reducing linearizability to state reachability. Inf. Comput. 261 (2018)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, Serdar Tasiran
Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency. ESOP (2017)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil
Proving Linearizability Using Forward Simulations. CAV (2) (2017)
Michael Emmi, Constantin Enea
Exposing Non-Atomic Methods of Concurrent Objects. CoRR (2017)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil
Proving linearizability using forward simulations. CoRR (2017)
Michael Emmi, Constantin Enea
Symbolic abstract data type inference. POPL (2016)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Michael Emmi
Verifying Constant-Time Implementations. USENIX Security Symposium (2016)
Montgomery Carter, Shaobo He, Jonathan Whitaker, Zvonimir Rakamaric, Michael Emmi
SMACK software verification toolchain. ICSE (Companion Volume) (2016)
Burcu Kulahcioglu Ozkan, Michael Emmi, Serdar Tasiran
Systematic Asynchrony Bug Exploration for Android Apps. CAV (1) (2015)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
On Reducing Linearizability to State Reachability. CoRR (2015)
Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, Zvonimir Rakamaric
SMACK+Corral: A Modular Verifier - (Competition Contribution). TACAS (2015)
Michael Emmi, Constantin Enea, Jad Hamza
Monitoring refinement via symbolic reasoning. PLDI (2015)
Michael Emmi, Pierre Ganty, Rupak Majumdar, Fernando Rosa-Velardo
Analysis of Asynchronous Programs with Event-Based Synchronization. ESOP (2015)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
On Reducing Linearizability to State Reachability. ICALP (2) (2015)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
Tractable Refinement Checking for Concurrent Objects. POPL (2015)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
Checking Correctness of Concurrent Objects: Tractable Reductions to Reachability (Invited Talk). FSTTCS (2015)
Ahmed Bouajjani, Michael Emmi
Bounded phase analysis of message-passing programs. Int. J. Softw. Tools Technol. Transf. 16 (2) (2014)
Zvonimir Rakamaric, Michael Emmi
SMACK: Decoupling Source Language Details from Verifier Implementations. CAV (2014)
Michael Emmi, Burcu Kulahcioglu Ozkan, Serdar Tasiran
Exploiting synchronization in the analysis of shared-memory asynchronous programs. SPIN (2014)
Ahmed Bouajjani, Michael Emmi
Analysis of Recursively Parallel Programs. ACM Trans. Program. Lang. Syst. 35 (3) (2013)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
Verifying Concurrent Programs against Sequential Specifications. ESOP (2013)
Michael Emmi, Akash Lal
Finding Non-terminating Executions in Distributed Asynchronous Programs. SAS (2012)
Michael Emmi, Akash Lal, Shaz Qadeer
Asynchronous programs with prioritized task-buffers. SIGSOFT FSE (2012)
Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi, Akash Lal
Detecting Fair Non-termination in Multithreaded Programs. CAV (2012)
Ahmed Bouajjani, Michael Emmi
Bounded Phase Analysis of Message-Passing Programs. TACAS (2012)
Ahmed Bouajjani, Michael Emmi
Analysis of recursively parallel programs. POPL (2012)
Ahmed Bouajjani, Michael Emmi, Gennaro Parlato
On Sequentializing Concurrent Programs. SAS (2011)
Michael Emmi, Shaz Qadeer, Zvonimir Rakamaric
Delay-bounded scheduling. POPL (2011)
Michael Emmi, Rupak Majumdar, Roman Manevich
Parameterized verification of transactional memories. PLDI (2010)
Michael Emmi, Ranjit Jhala, Eddie Kohler, Rupak Majumdar
Verifying Reference Counting Implementations. TACAS (2009)
Juan Chen, Chris Hawblitzel, Frances Perry, Michael Emmi, Jeremy Condit, Derrick Coetzee, Polyvios Pratikakis
Type-preserving compilation for large-scale optimizing object-oriented compilers. PLDI (2008)
Michael Emmi, Dimitra Giannakopoulou, Corina S. Pasareanu
Assume-Guarantee Verification for Interface Automata. FM (2008)
Michael Emmi, Rupak Majumdar, Koushik Sen
Dynamic test input generation for database applications. ISSTA (2007)
Michael Emmi, Jeffrey S. Fischer, Ranjit Jhala, Rupak Majumdar
Lock allocation. POPL (2007)
Alice Wang, Michael Emmi, Petros Faloutsos
Assembling an expressive facial animation system. Sandbox@SIGGRAPH (2007)
Michael Emmi, Rupak Majumdar
Verifying Compensating Transactions. VMCAI (2007)
Michael Emmi, Rupak Majumdar
Decision Problems for the Verification of Real-Time Software. HSCC (2006)