Characterizing Correctness Properties of Parallel Programs Using Fixpoints. - E. Allen Emerson; Edmund M. Clarke (ICALP, 1980)

Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. - E. Allen Emerson; Edmund M. Clarke (Sci. Comput. Program., 1982)

Deciding Branching Time Logic: A Triple Exponential Decision Procedure for CTL*. - E. Allen Emerson; A. Prasad Sistla (Logic of Programs, 1983)

Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach. - Edmund M. Clarke; E. Allen Emerson; A. Prasad Sistla (POPL, 1983)

"Sometimes" and "Not Never" Revisited: On Branching Versus Linear Time. - E. Allen Emerson; Joseph Y. Halpern (POPL, 1983)

Alternative Semantics for Temporal Logics. - E. Allen Emerson (Theor. Comput. Sci., 1983)

The Propositional Mu-Calculus is Elementary. - Robert S. Streett; E. Allen Emerson (ICALP, 1984)

Using Temporal Logic for Automatic Verification of Finite State Systems. - Edmund M. Clarke; Michael C. Browne; E. Allen Emerson; A. Prasad Sistla (Logics and Models of Concurrent Systems, 1984)

Deciding Branching Time Logic - E. Allen Emerson; A. Prasad Sistla (STOC, 1984)

Deciding Full Branching Time Logic - E. Allen Emerson; A. Prasad Sistla (Inf. Control., 1984)

Automata, Tableaux and Temporal Logics (Extended Abstract). - E. Allen Emerson (Logic of Programs, 1985)

Modalities for Model Checking: Branching Time Strikes Back. - E. Allen Emerson; Chin-Laung Lei (POPL, 1985)

Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. - E. Allen Emerson; Joseph Y. Halpern (J. Comput. Syst. Sci., 1985)

Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract) - E. Allen Emerson; Chin-Laung Lei (LICS, 1986)

Temporal Reasoning Under Generalized Fairness Constraints. - E. Allen Emerson; Chin-Laung Lei (STACS, 1986)

"Sometimes" and "Not Never" revisited: on branching versus linear time temporal logic. - E. Allen Emerson; Joseph Y. Halpern (J. ACM, 1986)

Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. - Edmund M. Clarke; E. Allen Emerson; A. Prasad Sistla (ACM Trans. Program. Lang. Syst., 1986)

Uniform Inevitability is Tree Automaton Ineffable. - E. Allen Emerson (Inf. Process. Lett., 1987)

Modalities for Model Checking: Branching Time Logic Strikes Back. - E. Allen Emerson; Chin-Laung Lei (Sci. Comput. Program., 1987)

The Complexity of Tree Automata and Logics of Programs (Extended Abstract) - E. Allen Emerson; Charanjit S. Jutla (FOCS, 1988)

Branching time temporal logic. - E. Allen Emerson; Jai Srinivasan (REX Workshop, 1988)

On Simultaneously Determinizing and Complementing omega-Automata (Extended Abstract) - E. Allen Emerson; Charanjit S. Jutla (LICS, 1989)

Synthesis of Concurrent Systems with Many Similar Sequential Processes. - Paul C. Attie; E. Allen Emerson (POPL, 1989)

Efficient Temporal Reasoning. - E. Allen Emerson; Tom Sadler; Jai Srinivasan (POPL, 1989)

An Automata Theoretic Decision Procedure for the Propositional Mu-Calculus - Robert S. Streett; E. Allen Emerson (Inf. Comput., 1989)

Temporal and Modal Logic. - E. Allen Emerson (Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), 1990)

On the Limits of Efficient Temporal Decidability (Extended Abstract) - E. Allen Emerson; Michael Evangelist; Jai Srinivasan (LICS, 1990)

A Decidable Temporal Logic to Reason About Many Processes. - E. Allen Emerson; Jai Srinivasan (PODC, 1990)

Tree Automata, Mu-Calculus and Determinacy (Extended Abstract) - E. Allen Emerson; Charanjit S. Jutla (FOCS, 1991)

Real-Time and the Mu-Calculus (Preliminary Report). - E. Allen Emerson (REX Workshop, 1991)

Formal Specification of Ssynchronous Distributed Real-Time Systems by APTL. - Farn Wang; Aloysius K. Mok; E. Allen Emerson (ICSE, 1992)

Efficient Temporal Satisfiability. - E. Allen Emerson; Tom Sadler; Jai Srinivasan (J. Log. Comput., 1992)

Quantitative Temporal Reasoning. - E. Allen Emerson; Aloysius K. Mok; A. Prasad Sistla; Jai Srinivasan (Real Time Syst., 1992)

On Model-Checking for Fragments of µ-Calculus. - E. Allen Emerson; Charanjit S. Jutla; A. Prasad Sistla (CAV, 1993)

Symbolic Model Checking for Distributed Real-Time Systems. - Farn Wang; Aloysius K. Mok; E. Allen Emerson (FME, 1993)

Distributed Real-Time System Specification and Verification in APTL. - Farn Wang; Aloysius K. Mok; E. Allen Emerson (ACM Trans. Softw. Eng. Methodol., 1993)

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; et al. (ICTAI, 1994)

Automated Temporal Reasoning about Reactive Systems. - E. Allen Emerson (Banff Higher Order Workshop, 1995)

Methods for Mu-calculus Model Checking: A Tutorial (Abstract). - E. Allen Emerson (CAV, 1995)

Efficient Automation of Temporal Reasoning. - E. Allen Emerson (CONCUR, 1995)

Modularity and Rule-Based Programming. - James C. Browne; E. Allen Emerson; Mohamed G. Gouda; Daniel P. Miranker; Aloysius K. Mok; Lance Obermeyer; F. Furman Haddix; Rwo-Hsi Wang; Sarah E. Chodrow (Int. J. Artif. Intell. Tools, 1995)

Automatic Verification of Parameterized Synchronous Systems (Extended Abstract). - E. Allen Emerson; Kedar S. Namjoshi (CAV, 1996)

Model Checking and the Mu-calculus. - E. Allen Emerson (Descriptive Complexity and Finite Models, 1996)

Synthesis of Concurrent Systems for an Atomic Read / Atomic Write Model of Computation (Extended Abstract). - Paul C. Attie; E. Allen Emerson (PODC, 1996)

Scheduling workflows by enforcing intertask dependencies. - Paul C. Attie; Munindar P. Singh; E. Allen Emerson; Amit P. Sheth; Marek Rusinkiewicz (Distributed Syst. Eng., 1996)

Symmetry and Model Checking. - E. Allen Emerson; A. Prasad Sistla (Formal Methods Syst. Des., 1996)

Checking Formal Specifications under Simulation. - William Canfield; E. Allen Emerson; Avijit Saha (ICCD, 1997)

Combining Partial Order and Symmetry Reductions. - E. Allen Emerson; Somesh Jha; Doron A. Peled (TACAS, 1997)

Generalized Quantitative Temporal Reasoning: An Automata Theoretic Approach. - E. Allen Emerson; Richard J. Trefler (TAPSOFT, 1997)

Utilizing Symmetry when Model-Checking under Fairness Assumptions: An Automata-Theoretic Approach. - E. Allen Emerson; A. Prasad Sistla (ACM Trans. Program. Lang. Syst., 1997)

Symmetry Reductions in Model Checking. - Edmund M. Clarke; E. Allen Emerson; Somesh Jha; A. Prasad Sistla (CAV, 1998)

Verification of Parameterized Bus Arbitration Protocol. - E. Allen Emerson; Kedar S. Namjoshi (CAV, 1998)

On Model Checking for Non-Deterministic Infinite-State Systems. - E. Allen Emerson; Kedar S. Namjoshi (LICS, 1998)

Model Checking Real-Time Properties of Symmetric Systems. - E. Allen Emerson; Richard J. Trefler (MFCS, 1998)

Synthesis of Concurrent Systems with Many Similar Processes. - Paul C. Attie; E. Allen Emerson (ACM Trans. Program. Lang. Syst., 1998)

Efficient Decompositional Model Checking for Regular Timing Diagrams. - Nina Amla; E. Allen Emerson; Kedar S. Namjoshi (CHARME, 1999)

From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking. - E. Allen Emerson; Richard J. Trefler (CHARME, 1999)

Parametric Quantitative Temporal Reasoning. - E. Allen Emerson; Richard J. Trefler (LICS, 1999)

The Complexity of Tree Automata and Logics of Programs. - E. Allen Emerson; Charanjit S. Jutla (SIAM J. Comput., 1999)

Reducing Model Checking of the Many to the Few. - E. Allen Emerson; Vineet Kahlon (CADE, 2000)

Model Checking Synchronous Timing Diagrams. - Nina Amla; E. Allen Emerson; Robert P. Kurshan; Kedar S. Namjoshi (FMCAD, 2000)

Model Checking: Theory into Practice. - E. Allen Emerson (FSTTCS, 2000)

Virtual Symmetry Reduction. - E. Allen Emerson; John Havlicek; Richard J. Trefler (LICS, 2000)

Automated formal methods: model checking and beyond. - E. Allen Emerson (ACM SIGSOFT Softw. Eng. Notes, 2000)

SMC: a symmetry-based model checker for verification of safety and liveness properties. - A. Prasad Sistla; Viktor Gyuris; E. Allen Emerson (ACM Trans. Softw. Eng. Methodol., 2000)

Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams. - Nina Amla; E. Allen Emerson; Robert P. Kurshan; Kedar S. Namjoshi (CAV, 2001)

Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams. - Nina Amla; E. Allen Emerson; Kedar S. Namjoshi; Richard J. Trefler (TACAS, 2001)

On model checking for the µ-calculus and its fragments. - E. Allen Emerson; Charanjit S. Jutla; A. Prasad Sistla (Theor. Comput. Sci., 2001)

Synthesis of concurrent programs for an atomic read/write model of computation. - Paul C. Attie; E. Allen Emerson (ACM Trans. Program. Lang. Syst., 2001)

Visual Specifications for Modular Reasoning about Asynchronous Systems. - Nina Amla; E. Allen Emerson; Kedar S. Namjoshi; Richard J. Trefler (FORTE, 2002)

Model Checking Large-Scale and Parameterized Resource Allocation Systems. - E. Allen Emerson; Vineet Kahlon (TACAS, 2002)

Exact and Efficient Verification of Parameterized Cache Coherence Protocols. - E. Allen Emerson; Vineet Kahlon (CHARME, 2003)

On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking. - E. Allen Emerson; Thomas Wahl (CHARME, 2003)

Abstract Patterns of Compositional Reasoning. - Nina Amla; E. Allen Emerson; Kedar S. Namjoshi; Richard J. Trefler (CONCUR, 2003)

Model Checking Guarded Protocols. - E. Allen Emerson; Vineet Kahlon (LICS, 2003)

Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols. - E. Allen Emerson; Vineet Kahlon (TACAS, 2003)

On Reasoning About Rings. - E. Allen Emerson; Kedar S. Namjoshi (Int. J. Found. Comput. Sci., 2003)

Parameterized Model Checking of Ring-Based Message Passing Systems. - E. Allen Emerson; Vineet Kahlon (CSL, 2004)

A Partitioning Methodology for BDD-Based Verification. - Debashis Sahoo; Subramanian K. Iyer; Jawahar Jain; Christian Stangier; Amit Narayan; David L. Dill; E. Allen Emerson (FMCAD, 2004)

Efficient Reduction Techniques for Systems with Many Components. - E. Allen Emerson; Thomas Wahl (SBMF, 2004)

Efficient Model Checking of Hardware Using Conditioned Slicing. - Shobha Vasudevan; E. Allen Emerson; Jacob A. Abraham (AVoCS, 2004)

Synthesis of fault-tolerant concurrent programs. - Paul C. Attie; Anish Arora; E. Allen Emerson (ACM Trans. Program. Lang. Syst., 2004)

Predictive Reachability Using a Sample-Based Approach. - Debashis Sahoo; Jawahar Jain; Subramanian K. Iyer; David L. Dill; E. Allen Emerson (CHARME, 2005)

Multi-threaded reachability. - Debashis Sahoo; Jawahar Jain; Subramanian K. Iyer; David L. Dill; E. Allen Emerson (DAC, 2005)

Dynamic Symmetry Reduction. - E. Allen Emerson; Thomas Wahl (TACAS, 2005)

Under-approximation Heuristics for Grid-based Bounded Model Checking. - Subramanian K. Iyer; Jawahar Jain; Debashis Sahoo; E. Allen Emerson (PDMC@ICALP, 2005)

Reducing Model Checking of the Few to the One. - E. Allen Emerson; Richard J. Trefler; Thomas Wahl (ICFEM, 2006)

Automatic Verification of Parameterized Data Structures. - Jyotirmoy V. Deshmukh; E. Allen Emerson; Prateek Gupta (TACAS, 2006)

Molecular Model Checking. - E. Allen Emerson; Kristina D. Hager; Jay H. Konieczka (Int. J. Found. Comput. Sci., 2006)

On partitioning and symbolic model checking. - Subramanian K. Iyer; Debashis Sahoo; E. Allen Emerson; Jawahar Jain (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2006)

Improved verification of hardware designs through antecedent conditioned slicing. - Shobha Vasudevan; E. Allen Emerson; Jacob A. Abraham (Int. J. Softw. Tools Technol. Transf., 2007)

Automatic Generation of Local Repairs for Boolean Programs. - Roopsha Samanta; Jyotirmoy V. Deshmukh; E. Allen Emerson (FMCAD, 2008)

Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. - Edmund M. Clarke; E. Allen Emerson (25 Years of Model Checking, 2008)

The Beginning of Model Checking: A Personal Perspective. - E. Allen Emerson (25 Years of Model Checking, 2008)

SVISS: Symbolic Verification of Symmetric Systems. - Thomas Wahl; Nicolas Blanc; E. Allen Emerson (TACAS, 2008)

Verification of recursive methods on tree-like data structures. - Jyotirmoy V. Deshmukh; E. Allen Emerson (FMCAD, 2009)

Symbolic Deadlock Analysis in Concurrent Libraries and Their Clients. - Jyotirmoy V. Deshmukh; E. Allen Emerson; Sriram Sankaranarayanan 001 (ASE, 2009)

Model Checking: Progress and Problems. - E. Allen Emerson (VMCAI, 2009)

Model checking: algorithmic verification and debugging. - Edmund M. Clarke; E. Allen Emerson; Joseph Sifakis (Commun. ACM, 2009)

Meanings of Model Checking. - E. Allen Emerson (Concurrency, Compositionality, and Correctness, 2010)

Time of Time. - E. Allen Emerson (SAS, 2010)

An Algorithmic Framework for Synthesis of Concurrent Programs. - E. Allen Emerson; Roopsha Samanta (ATVA, 2011)

A More Efficient BDD-Based QBF Solver. - Oswaldo Olivo; E. Allen Emerson (CP, 2011)

Symbolic modular deadlock analysis. - Jyotirmoy V. Deshmukh; E. Allen Emerson; Sriram Sankaranarayanan 001 (Autom. Softw. Eng., 2011)

Systems Architecture, Design, Engineering, and Verification - The Practice in Research and Research in Practice. - Dahlia Malkhi; Fernando J. Corbató; E. Allen Emerson; Joseph Sifakis; Ken Thompson (ACM-TURING, 2012)

Improved Binary Decision Diagram Constraint Propagation for Satisfiability Problems. - Oswaldo Olivo; E. Allen Emerson (SCCC, 2012)

Cost-Aware Automatic Program Repair. - Roopsha Samanta; Oswaldo Olivo; E. Allen Emerson (SAS, 2014)

Memories of Edsger W. Dijkstra. - E. Allen Emerson (Edsger Wybe Dijkstra, 2022)