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.

Professional Activities

Program Committee CAV ’25
Program Committee CSF ’25
Program Committee POPL ’25
Program Committee PLDI ’24
Program Committee VMCAI ’24
Program Committee CSF ’24
Program Committee SAS ’23
Program Committee CAV ’23
Program Chair VMCAI ’23
Program Committee CSF ’23
Program Committee ESOP ’23
Program Chair DSV ’22
Program Committee ATVA ’22
Program Committee CSF ’22
Program Committee POPL ’22
Program Committee SAS ’21
Program Committee CSF ’21
External Review Committee OOPSLA ’20
Program Committee CONCUR ’20
Program Committee CAV ’20
Program Chair DSV ’20
Selection Committee PL Day ’19
Program Committee PLDI ’19
Program Committee POPL ’19
Program Chair DSV ’19
Contributed Talk NYPLSE ’19
Review Panelist NSF ‘19
Contributed Talk PL Day ’18
Program Committee LPAR-22
Invited Talk AVoCS ’18
Invited Talk FRIDA ’18
Program Committee YR-CONCUR ’18
Invited Talk VSSE ’18
Program Committee SecDev ’18
Program Committee NETYS ’18
Program Committee CAV ’18
Review Panelist NSF ‘17
Program Committee TAPAS ’17
Contributed Talk PL Day ’17
Program Committee CAV ’17
Program Committee FORTE ’17
Program Committee FoSSaCS ’17
Contributed Talk NJPLS ’16
Invited Talk FMS ’16
Program Committee EC2 ’16
Program Committee FMCAD ’16
Program Committee NETYS ’16
External Review Committee POPL ’16
External Review Committee PPoPP ’16
Program Committee EC2 ’15
External Review Committee POPL ’15
Invited Talk CCDP ’15
Program Committee FM ’15
Program Chair EC2 ’14
External Review Committee PLDI ’14
External Review Committee POPL ’13
Program Committee VMCAI ’13
Program Committee Bytecode ’11

Publications

Compositional Taint Analysis for Enforcing Security Policies at Scale ESEC/FSE ’23
RAPID: Checking API Usage for the Cloud in the Cloud ESEC/FSE ’21
Behavioral Simulation for Smart Contracts PLDI ’20
Verifying Visibility-Based Weak Consistency ESOP ’20
ct-fuzz: Fuzzing for Timing Leaks ICST ’20
On the Complexity of Checking Consistency for Replicated Data Types CAV ’19
Violat: Generating Tests of Observational Refinement for Concurrent Objects CAV ’19
Weak-Consistency Specification via Visibility Relaxation POPL ’19
SideTrail: Verifying Time-Balancing of Cryptosystems VSTTE ’18
Monitoring Weak Consistency CAV ’18
On Reducing Linearizability to State Reachability IC ’18
Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections POPL ’18
Exposing Non-Atomic Methods of Concurrent Objects arXiv ’17
Proving Linearizability Using Forward Simulations CAV ’17
Verifying Robustness of Event-Driven Asynchronous Programs against Concurrency ESOP ’17
Verifying Constant-Time Implementations USENIX Security ’16
SMACK Software Verification Toolchain ICSE Companion ’16
Symbolic Abstract Data Type Inference POPL ’16
Systematic Asynchrony Bug Exploration for Android Apps CAV ’15
Checking Correctness of Concurrent Objects: Tractable Reductions to Reachability (Invited Talk) FSTTCS ’15
On Reducing Linearizability to State Reachability ICALP ’15
Monitoring Refinement via Symbolic Reasoning PLDI ’15
SMACK+Corral: A Modular Verifier (Competition Contribution) TACAS ’15
Analysis of Asynchronous Programs with Event-Based Synchronization ESOP ’15
Tractable Refinement Checking for Concurrent Objects POPL ’15
SMACK: Decoupling Source Language Details from Verifier Implementations CAV ’14
Exploiting Synchronization in the Analysis of Shared-Memory Asynchronous Programs SPIN ’14
Bounded Phase Analysis of Message-Passing Programs STTT ’14
Verifying Concurrent Programs Against Sequential Specifications ESOP ’13
Analysis of Recursively Parallel Programs TOPLAS ’13
Asynchronous Programs with Prioritized Task-Buffers FSE ’12
Finding Non-Terminating Executions in Distributed Asynchronous Programs SAS ’12
Detecting Fair Non-Termination in Multithreaded Programs CAV ’12
Bounded Phase Analysis of Message-Passing Programs TACAS ’12
Analysis of Recursively Parallel Programs POPL ’12
On Sequentializing Concurrent Programs SAS ’11
Delay-Bounded Scheduling POPL ’11
Parameterized Verification of Transactional Memories PLDI ’10
Verifying Reference Counting Implementations TACAS ’09
Assume-Guarantee Verification for Interface Automata FM ’08
Type-Preserving Compilation for Large-Scale Optimizing Object-Oriented Compilers PLDI ’08
Assembling an Expressive Facial Animation System Sandbox ’07
Dynamic Test Input Generation for Database Applications ISSTA ’07
Verifying Compensating Transactions VMCAI ’07
Lock Allocation POPL ’07
Decision Problems for the Verification of Real-Time Software HSCC ’06

Software

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

Contact

michael.emmi@gmail.com