About

Michael received his doctorate in Computer Science from UCLA in 2010 and joined Amazon Web Services (AWS) in 2019, following a postdoc fellowship at the Paris 7 awarded by La Fondation Sciences Mathématiques de Paris (FSMP), and faculty researcher positions at the IMDEA Software Institute, Nokia Bell Labs, and SRI International. Prior to all that, Michael completed his undergraduate studies at Binghamton University (SUNY). He has been a teaching assistant for undergraduate courses at UCLA and Paris 7, and has held internships at Microsoft Research, NASA Ames Research Center, and IBM.

Michael’s research enables the construction of reliable software by developing the foundations for effective programming abstractions and informative program analysis tools. Integrating technological trends with knowledge from several research communities spanning automata theory, programming languages, and distributed systems, his contributions include establishing the theoretical limits of program analysis, devising tractable approximations for intractable analysis problems, and building effective analysis tools.

Education

Ph.D. Computer Science. University of California, Los Angeles (UCLA), 2010.
M.S. Computer Science. University of California, Los Angeles (UCLA), 2005.
B.S. Computer Science. Binghamton University (SUNY), 2003.

Awards

Postdoctoral Fellowship. La Fondation Sciences Mathématiques de Paris (FSMP), 2010–2012.

Employment

Applied Scientist. Amazon Web Services, New York, NY, 2019–present.
Sr. Computer Scientist. SRI International, 2017–2019.
Member of Technical Staff. Nokia Bell Labs, Murray Hill, NJ, 2016–2017.
Researcher. IMDEA Software Institute, Madrid, 2013–2016.
Postdoc Researcher. LIAFA, Universtié Paris Diderot, 2010–2013.
Lecturer (ATER). Paris 7, 2012–2013.
Visiting Researcher. Microsoft Research, Bangalore, 2011.
Research Intern. Microsoft Research, Redmond, 2010.
Research Intern. Microsoft Research, Cambridge (UK), 2008.
Research Intern. Microsoft Research, Redmond, 2007.
Research Intern. NASA Ames Research Center, 2006.
Research Assistant. University of California, Los Angeles (UCLA), 2006–2010.
Teaching Assistant. University of California, Los Angeles (UCLA), 2003–2005.
Software Engineer Intern. IBM, Endicott, 2001, 2002.
Course Assistant. Binghamton University (SUNY), 2001–2002.

References

Ahmed Bouajjani. Professor, Université Paris Diderot. abou@irif.fr
Rupak Majumdar. Scientific Director, MPI-SWS. rupak@mpi-sws.org
Shaz Qadeer. Research Scientist, Facebook Research.
Dimitra Giannakopoulou. Research Computer Scientist, NASA Ames Research Center. Dimitra.Giannakopoulou@nasa.gov
Josh Berdine. Software Engineer, Facebook Research.

Activities

Program Committee. 31st International Conference on Concurrency Theory (CONCUR ’20).
Program Committee. 32nd International Conference on Computer Aided Verification (CAV ’20).
Selection Committee. IBM Programming Languages Day (PL Day ’19).
Program Committee. 40th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI ’19).
Program Committee. 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL ’19).
Program Chair. Workshop on Democratizing Software Verification (DSV ’19).
Contributed Talk. New York Seminar on Programming Languages and Software Engineering (NYPLSE ’19).
Review Panelist. The National Science Foundation (NSF ‘19).
Contributed Talk. IBM Programming Languages Day (PL Day ’18).
Program Committee. 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-22).
Invited Talk. 18th International Workshop on Automated Verification of Critical Systems (AVoCS ’18).
Invited Talk. The 5th Workshop on Formal Reasoning in Distributed Algorithms (FRIDA ’18).
Program Committee. 8th Young Researchers Workshop on Concurrency Theory (YR-CONCUR ’18).
Invited Talk. Workshop on Verification and Synthesis for Software Evolution (VSSE ’18).
Program Committee. IEEE Cybersecurity Development Conference (SecDev ’18).
Program Committee. 6th International Conference on Networked Systems (NETYS ’18).
Program Committee. 30th International Conference on Computer Aided Verification (CAV ’18).
Review Panelist. The National Science Foundation (NSF ‘17).
Program Committee. 8th Workshop on Tools for Automatic Program Analysis (TAPAS ’17).
Contributed Talk. IBM Programming Languages Day (PL Day ’17).
Program Committee. 29th International Conference on Computer-Aided Verification (CAV ’17).
Program Committee. 37th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE ’17).
Program Committee. 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS ’17).
Contributed Talk. NJ Programming Languages and Systems Seminar (NJPLS ’16).
Invited Talk. Workshop on Formal Methods and Security (FMS ’16).
Program Committee. 9th International Workshop on Exploiting Concurrency Efficiently and Correctly (EC2 ’16).
Program Committee. 16th International Conference on Formal Methods in Computer-Aided Design (FMCAD ’16).
Program Committee. 4th International Conference on Networked Systems (NETYS ’16).
External Review Committee. 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16).
External Review Committee. 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP ’16).
Program Committee. 8th International Workshop on Exploiting Concurrency Efficiently and Correctly (EC2 ’15).
External Review Committee. 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15).
Invited Talk. 2nd Workshop on The Chemistry of Concurrent and Distributed Programming (CCDP ’15).
Program Committee. 20th International Symposium on Formal Methods (FM ’15).
Program Chair. 7th International Workshop on Exploiting Concurrency Efficiently and Correctly (EC2 ’14).
External Review Committee. 35th annual ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’14).
External Review Committee. 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’13).
Program Committee. 14th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI ’13).
Program Committee. 6th International Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode ’11).

Publications

Siddharth Krishna, Michael Emmi, Constantin Enea, Dejan Jovanovic. Verifying Visibility-Based Weak Consistency. ArXiv e-prints, 2019. (PDF)
Ranadeep Biswas, Michael Emmi, and Constantin Enea. On the Complexity of Checking Consistency for Replicated Data Types. In Proc. 31st International Conference on Computer Aided Verification (CAV ’19), LNCS, volume 11562, pages 324–343. Springer, 2019. (PDF)
Michael Emmi and Constantin Enea. Violat: Generating Tests of Observational Refinement for Concurrent Objects. In Proc. 31st International Conference on Computer Aided Verification (CAV ’19), LNCS, volume 11562, pages 534–546. Springer, 2019. (PDF)
Michael Emmi, Shaobo He, and Gabriela Ciocarlie. ct-fuzz: Fuzzing for Timing Leaks. ArXiv e-prints, 2019. (PDF)
Michael Emmi and Constantin Enea. Weak-Consistency Specification via Visibility Relaxation. In Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL ’19), pages 60:1–60:28. ACM, 2019. (PDF)
Konstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCarthaigh, Daniel Schwartz-Narbonne and Serdar Tasiran. SideTrail: Verifying Time-Balancing of Cryptosystems. In Proc. 10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE ’18), LNCS, volume 11294, pages 215–228. Springer, 2018. (PDF)
Michael Emmi and Constantin Enea. Monitoring Weak Consistency. In Proc. 30th International Conference on Computer Aided Verification (CAV ’18), LNCS, volume 10981, pages 487–506. Springer, 2018. (PDF)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. On Reducing Linearizability to State Reachability. In Information and Computation (IC ’18), volume 261, pages 383–400. Elsevier, 2018. (PDF)
Michael Emmi and Constantin Enea. Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections. In Proc. 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL ’18), pages 25:1–25:27. ACM, 2018. (PDF)
Michael Emmi and Constantin Enea. Exposing Non-Atomic Methods of Concurrent Objects. ArXiv e-prints, 2017. (PDF)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Suha Orhun Mutluergil. Proving Linearizability Using Forward Simulations. In Proc. 29th International Conference on Computer-Aided Verification (CAV ’17), LNCS, volume 10427, pages 542–563. Springer, 2017. (PDF)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, and Serdar Tasiran. Verifying Robustness of Event-Driven Asynchronous Programs against Concurrency. In Proc. 26th European Symposium on Programming (ESOP ’17), LNCS, volume 10201, pages 170–200. Springer, 2017. (PDF)
Jose Carlos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi. Verifying Constant-Time Implementations. In Proc. 25th USENIX Security Symposium (USENIX Security ’16), pages 53–70. USENIX Association, 2016. (PDF)
Montgomery Carter, Shaobo He, Jonathan Whitaker, Zvonimir Rakamaric, and Michael Emmi. SMACK Software Verification Toolchain. In Proc. 38th International Conference on Software Engineering (ICSE Companion ’16), pages 589–592. ACM, 2016. (PDF)
Michael Emmi and Constantin Enea. Symbolic Abstract Data Type Inference. In Proc. 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16), pages 513–525. ACM, 2016. (PDF)
Burcu Kulahcioglu Ozkan, Michael Emmi, and Serdar Tasiran. Systematic Asynchrony Bug Exploration for Android Apps. In Proc. 27th International Conference on Computer Aided Verification (CAV ’15), LNCS, volume 9206, pages 455–461. Springer, 2015. (PDF)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. Checking Correctness of Concurrent Objects: Tractable Reductions to Reachability (Invited Talk). In Proc. 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS ’15), LIPIcs, volume 45, pages 95–107. Schloss Dagstuhl — Leibniz-Zentrum fuer Informatik, 2015. (PDF)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. On Reducing Linearizability to State Reachability. In Proc. 42nd International Colloquium on Automata, Languages, and Programming (ICALP ’15), LNCS, volume 9135, pages 95–107. Springer, 2015. (PDF)
Michael Emmi, Constantin Enea, and Jad Hamza. Monitoring Refinement via Symbolic Reasoning. In Proc. 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI ’15), pages 260–269. ACM, 2015. (PDF)
Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, and Zvonimir Rakamaric. SMACK+Corral: A Modular Verifier (Competition Contribution). In Proc. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’15), LNCS, volume 9035, pages 451–454. Springer, 2015. (PDF)
Michael Emmi, Pierre Ganty, Rupak Majumdar, and Fernando Rosa-Velardo. Analysis of Asynchronous Programs with Event-Based Synchronization. In Proc. 24th European Symposium on Programming, (ESOP ’15), LNCS, volume 9032, pages 535–559. Springer, 2015. (PDF)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. Tractable Refinement Checking for Concurrent Objects. In Proc. 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15), pages 651–662. ACM, 2015. (PDF)
Zvonimir Rakamaric and Michael Emmi. SMACK: Decoupling Source Language Details from Verifier Implementations. In Proc. 26th International Conference on Computer Aided Verification (CAV ’14), LNCS, volume 8559, pages 106–113. Springer, 2014. (PDF)
Michael Emmi, Burcu Kulahcioglu Ozkan, and Serdar Tasiran. Exploiting Synchronization in the Analysis of Shared-Memory Asynchronous Programs. In Proc. International SPIN Symposium on Model Checking of Software (SPIN ’14), pages 20–29. ACM, 2014. (PDF)
Ahmed Bouajjani and Michael Emmi. Bounded Phase Analysis of Message-Passing Programs. In International Journal on Software Tools for Technology Transfer (STTT ’14), volume 16, issue 2, pages 127–146. Springer, 2014. (PDF)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. Verifying Concurrent Programs Against Sequential Specifications. In Proc. 22nd European Symposium on Programming (ESOP ’13), LNCS, volume 7792, pages 290–309. Springer, 2013. (PDF)
Ahmed Bouajjani and Michael Emmi. Analysis of Recursively Parallel Programs. In ACM Transactions on Programming Languages and Systems (TOPLAS ’13), volume 35, issue 3, pages 10:1–10:49. ACM, 2013. (PDF)
Michael Emmi, Akash Lal, and Shaz Qadeer. Asynchronous Programs with Prioritized Task-Buffers. In Proc. 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE ’12), pages 48. ACM, 2012. (PDF)
Michael Emmi and Akash Lal. Finding Non-Terminating Executions in Distributed Asynchronous Programs. In Proc. 19th International Static Analysis Symposium (SAS ’12), LNCS, volume 7460, pages 439–455. Springer, 2012. (PDF)
Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi, and Akash Lal. Detecting Fair Non-Termination in Multithreaded Programs. In Proc. 24th International Conference on Computer Aided Verification (CAV ’12), LNCS, volume 7358, pages 210–226. Springer, 2012. (PDF)
Ahmed Bouajjani and Michael Emmi. Bounded Phase Analysis of Message-Passing Programs. In Proc. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’12), LNCS, volume 7214, pages 451–465. Springer, 2012. (PDF)
Ahmed Bouajjani and Michael Emmi. Analysis of Recursively Parallel Programs. In Proc. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’12), pages 203–214. ACM, 2012. (PDF)
Ahmed Bouajjani, Michael Emmi, and Gennaro Parlato. On Sequentializing Concurrent Programs. In Proc. 18th International Symposium on Static Analysis (SAS ’11), LNCS, volume 6887, pages 129–145. Springer, 2011. (PDF)
Michael Emmi, Shaz Qadeer, and Zvonimir Rakamaric. Delay-Bounded Scheduling. In Proc. 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’11), pages 411–422. ACM, 2011. (PDF)
Michael Emmi, Rupak Majumdar, and Roman Manevich. Parameterized Verification of Transactional Memories. In Proc. ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation (PLDI ’10), pages 134–145. ACM, 2010. (PDF)
Michael Emmi, Ranji Jhala, Eddie Kohler, and Rupak Majumdar. Verifying Reference Counting Implementations. In Proc. 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’09), LNCS, volume 5505, pages 352–367. Springer, 2009. (PDF)
Michael Emmi, Dimitra Giannakopoulou, and Corina S. Pasareanu. Assume-Guarantee Verification for Interface Automata. In Proc. 15th International Symposium on Formal Methods (FM ’08), LNCS, volume 5014, pages 116–131. Springer, 2008. (PDF)
Juan Chen, Chris Hawblitzel, Frances Perry, Michael Emmi, Jeremy Condit, Derrick Coetzee, and Polyvios Pratikakis. Type-Preserving Compilation for Large-Scale Optimizing Object-Oriented Compilers. In Proc. ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI ’08), pages 183–192. ACM, 2008. (PDF)
Alice Wang, Michael Emmi, and Petros Faloutsos. Assembling an Expressive Facial Animation System. In Proc. ACM SIGGRAPH Symposium on Video Games (Sandbox ’07), pages 21–26. ACM, 2007. (PDF)
Michael Emmi, Rupak Majumdar, and Koushik Sen. Dynamic Test Input Generation for Database Applications. In Proc. ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA ’07), pages 151–162. ACM, 2007. (PDF)
Michael Emmi and Rupak Majumdar. Verifying Compensating Transactions. In Proc. 8th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI ’07), LNCS, volume 4349, pages 29–43. Springer, 2007. (PDF)
Michael Emmi, Jeff Fischer, Ranjit Jhala, and Rupak Majumdar. Lock Allocation. In Proc. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’07), pages 291–296. ACM, 2007. (PDF)
Michael Emmi and Rupak Majumdar. Decision Problems for the Verification of Real-Time Software. In Proc. 9th International Workshop on Hybrid Systems: Computation and Control (HSCC ’06), LNCS, volume 3927, pages 200–211. Springer, 2006. (PDF)

Collaborators and Coauthors

José Bacelar Almeida (Universidade do Minho) Mohamed Faouzi Atig (Uppsala University) Manuel Barbosa (University of Porto) Gilles Barthe (IMDEA Software) Ahmed Bouajjani (Paris 7) Montgomery Carter (University of Utah) Juan Chen (MSR) Gabriela Ciocarlie (SRI International) Derrick Coetzee (MSR) Jeremy Condit (MSR) François Dupressoir (IMDEA Software) Constantin Enea (Paris 7) Petros Faloutsos (UCLA) Jeffrey S. Fischer (UCLA) Pierre Ganty (IMDEA Software) Dimitra Giannakopoulou (NASA Ames) Jad Hamza (Paris 7) Arvind Haran (University of Utah) Chris Hawblitzel (MSR) Shaobo He (University of Utah) Ranjit Jhala (UCSD) Eddie Kohler (Harvard) Akash Lal (MSR) Rupak Majumdar (MPI-SWS) Roman Manevich (UCLA) Kedar Namjoshi (Nokia Bell Labs) Burcu Kulahcioglu Ozkan (Koç University) Gennaro Parlato (Paris 7) Corina S. Pasareanu (NASA Ames) Frances Perry (Princeton University) Polyvios Pratikaki (University of Maryland) Shaz Qadeer (MSR) Zvonimir Rakamaric (University of Utah) Fernando Rosa-Velardo (Universidad Complutense de Madrid) Koushik Sen (University of California, Berkeley) Serdar Tasiran (Koç University) Alice Wang (UCLA) Jonathan Whitaker (University of Utah)

Software

SMACK, SV-COMP award-winning bounded software verifier for C programs. https://github.com/smackers/smack
ct-verif, a tool for verifying constant time implementations, and a case study of verified constant-time implementations. https://github.com/imdea-software/verifying-constant-time
Violat, discovers simple test harnesses which demonstrate violations to atomicity — and weak-consistency — of Java concurrent data structures. https://github.com/michael-emmi/violat
Violin, efficient symbolic reasoning algorithms for checking linearizability of concurrent data structures. https://github.com/imdea-software/violin
BAM! BAM! Boogieman, Boogie AST Manipulator which implements various code analyses and transformations for the Boogie intermediate verification language. https://github.com/michael-emmi/bam-bam-boogieman
Bibly, simplifies the creation and maintenance of bibliographies in LaTeX documents by fetching the BibTex entries corresponding to LaTeX citations. https://github.com/michael-emmi/bibly
2up, save paper by printing every two pages on a single page. https://github.com/michael-emmi/2up