| 2014 | SAS | Cost-Aware Automatic Program Repair. | Roopsha Samanta, Oswaldo Olivo, E. Allen Emerson |
| 2011 | ATVA | An Algorithmic Framework for Synthesis of Concurrent Programs. | E. Allen Emerson, Roopsha Samanta |
| 2011 | CP | A More Efficient BDD-Based QBF Solver. | Oswaldo Olivo, E. Allen Emerson |
| 2010 | SAS | Time of Time. | E. Allen Emerson |
| 2009 | FMCAD | Verification of recursive methods on tree-like data structures. | Jyotirmoy V. Deshmukh, E. Allen Emerson |
| 2009 | VMCAI | Model Checking: Progress and Problems. | E. Allen Emerson |
| 2008 | FMCAD | Automatic Generation of Local Repairs for Boolean Programs. | Roopsha Samanta, Jyotirmoy V. Deshmukh, E. Allen Emerson |
| 2008 | TACAS | SVISS: Symbolic Verification of Symmetric Systems. | Thomas Wahl, Nicolas Blanc, E. Allen Emerson |
| 2006 | ICFEM | Reducing Model Checking of the Few to the One. | E. Allen Emerson, Richard J. Trefler, Thomas Wahl |
| 2006 | TACAS | Automatic Verification of Parameterized Data Structures. | Jyotirmoy V. Deshmukh, E. Allen Emerson, Prateek Gupta |
| 2005 | DAC | Multi-threaded reachability. | Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill, E. Allen Emerson |
| 2005 | FM | On Partitioning and Symbolic Model Checking. | Subramanian K. Iyer, Debashis Sahoo, E. Allen Emerson, Jawahar Jain |
| 2005 | TACAS | Dynamic Symmetry Reduction. | E. Allen Emerson, Thomas Wahl |
| 2004 | CSL | Parameterized Model Checking of Ring-Based Message Passing Systems. | E. Allen Emerson, Vineet Kahlon |
| 2004 | FMCAD | A Partitioning Methodology for BDD-Based Verification. | Debashis Sahoo, Subramanian K. Iyer, Jawahar Jain, Christian Stangier, Amit Narayan, David L. Dill, E. Allen Emerson |
| 2003 | CONCUR | Abstract Patterns of Compositional Reasoning. | Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler |
| 2003 | LICS | Model Checking Guarded Protocols. | E. Allen Emerson, Vineet Kahlon |
| 2003 | TACAS | Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols. | E. Allen Emerson, Vineet Kahlon |
| 2002 | FORTE | Visual Specifications for Modular Reasoning about Asynchronous Systems. | Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler |
| 2002 | TACAS | Model Checking Large-Scale and Parameterized Resource Allocation Systems. | E. Allen Emerson, Vineet Kahlon |
| 2001 | CAV | Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams. | Nina Amla, E. Allen Emerson, Robert P. Kurshan, Kedar S. Namjoshi |
| 2001 | TACAS | Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams. | Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler |
| 2000 | CADE | Reducing Model Checking of the Many to the Few. | E. Allen Emerson, Vineet Kahlon |
| 2000 | FMCAD | Model Checking Synchronous Timing Diagrams. | Nina Amla, E. Allen Emerson, Robert P. Kurshan, Kedar S. Namjoshi |
| 2000 | LICS | Virtual Symmetry Reduction. | E. Allen Emerson, John Havlicek, Richard J. Trefler |
| 1999 | LICS | Parametric Quantitative Temporal Reasoning. | E. Allen Emerson, Richard J. Trefler |
| 1998 | CAV | Symmetry Reductions in Model Checking. | Edmund M. Clarke, E. Allen Emerson, Somesh Jha, A. Prasad Sistla |
| 1998 | CAV | Verification of Parameterized Bus Arbitration Protocol. | E. Allen Emerson, Kedar S. Namjoshi |
| 1998 | LICS | On Model Checking for Non-Deterministic Infinite-State Systems. | E. Allen Emerson, Kedar S. Namjoshi |
| 1998 | MFCS | Model Checking Real-Time Properties of Symmetric Systems. | E. Allen Emerson, Richard J. Trefler |
| 1998 | PODC | Synthesis of Fault-Tolerant Concurrent Programs. | Anish Arora, Paul C. Attie, E. Allen Emerson |
| 1997 | ICCD | Checking Formal Specifications under Simulation. | William Canfield, E. Allen Emerson, Avijit Saha |
| 1997 | TACAS | Combining Partial Order and Symmetry Reductions. | E. Allen Emerson, Somesh Jha, Doron A. Peled |
| 1996 | CAV | Automatic Verification of Parameterized Synchronous Systems (Extended Abstract). | E. Allen Emerson, Kedar S. Namjoshi |
| 1996 | PODC | Synthesis of Concurrent Systems for an Atomic Read / Atomic Write Model of Computation (Extended Abstract). | Paul C. Attie, E. Allen Emerson |
| 1995 | CAV | Methods for Mu-calculus Model Checking: A Tutorial (Abstract). | E. Allen Emerson |
| 1995 | CAV | Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic Approach. | E. Allen Emerson, A. Prasad Sistla |
| 1995 | CONCUR | Efficient Automation of Temporal Reasoning. | E. Allen Emerson |
| 1995 | POPL | Reasoning about Rings. | E. Allen Emerson, Kedar S. Namjoshi |
| 1994 | ICTAI | A New Approach to Modularity in Rule-Based Programming. | James C. Browne, E. Allen Emerson, Mohamed G. Gouda, Daniel P. Miranker, Aloysius K. Mok, Roberto J. Bayardo Jr., Sarah E. Chodrow, David Gadbois, F. Furman Haddix, Thomas W. Hetherington, Lance Obermeyer, Duu-Chung Tsou, Chih-Kan Wang, Rwo-Hsi Wang |
| 1993 | CAV | On Model-Checking for Fragments of µ-Calculus. | E. Allen Emerson, Charanjit S. Jutla, A. Prasad Sistla |
| 1993 | CAV | Symmetry and Model Checking. | E. Allen Emerson, A. Prasad Sistla |
| 1993 | FM | Symbolic Model Checking for Distributed Real-Time Systems. | Farn Wang, Aloysius K. Mok, E. Allen Emerson |
| 1992 | ICSE | Formal Specification of Ssynchronous Distributed Real-Time Systems by APTL. | Farn Wang, Aloysius K. Mok, E. Allen Emerson |
| 1991 | FOCS | Tree Automata, Mu-Calculus and Determinacy (Extended Abstract) | E. Allen Emerson, Charanjit S. Jutla |
| 1990 | CAV | Quantitative Temporal Reasoning. | E. Allen Emerson, Aloysius K. Mok, A. Prasad Sistla, Jai Srinivasan |
| 1990 | LICS | On the Limits of Efficient Temporal Decidability (Extended Abstract) | E. Allen Emerson, Michael Evangelist, Jai Srinivasan |
| 1990 | PODC | A Decidable Temporal Logic to Reason About Many Processes. | E. Allen Emerson, Jai Srinivasan |
| 1989 | LICS | On Simultaneously Determinizing and Complementing omega-Automata (Extended Abstract) | E. Allen Emerson, Charanjit S. Jutla |
| 1989 | POPL | Synthesis of Concurrent Systems with Many Similar Sequential Processes. | Paul C. Attie, E. Allen Emerson |
| 1989 | POPL | Efficient Temporal Reasoning. | E. Allen Emerson, Tom Sadler, Jai Srinivasan |
| 1988 | FOCS | The Complexity of Tree Automata and Logics of Programs (Extended Abstract) | E. Allen Emerson, Charanjit S. Jutla |
| 1986 | LICS | Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract) | E. Allen Emerson, Chin-Laung Lei |
| 1986 | STACS | Temporal Reasoning Under Generalized Fairness Constraints. | E. Allen Emerson, Chin-Laung Lei |
| 1985 | POPL | Modalities for Model Checking: Branching Time Strikes Back. | E. Allen Emerson, Chin-Laung Lei |
| 1984 | ICALP | The Propositional Mu-Calculus is Elementary. | Robert S. Streett, E. Allen Emerson |
| 1984 | STOC | Deciding Branching Time Logic | E. Allen Emerson, A. Prasad Sistla |
| 1983 | POPL | Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach. | Edmund M. Clarke, E. Allen Emerson, A. Prasad Sistla |
| 1983 | POPL | "Sometimes" and "Not Never" Revisited: On Branching Versus Linear Time. | E. Allen Emerson, Joseph Y. Halpern |
| 1982 | STOC | Decision Procedures and Expressiveness in the Temporal Logic of Branching Time | E. Allen Emerson, Joseph Y. Halpern |
| 1980 | ICALP | Characterizing Correctness Properties of Parallel Programs Using Fixpoints. | E. Allen Emerson, Edmund M. Clarke |