Papers     Technical Reports     Theses

Papers

• [PS] E. Allen Emerson. Automated Temporal Reasoning about Reactive Systems, BANFF Higher Order Logics for Concurrency: Structure vs Automata, LNCS 1043, 1996.

• [PS] E. Allen Emerson. Model Checking and the Mu-calculus, In N. Immerman and P. G. Kolaitis, eds., Descriptive Complexity and Finite Models, volume 31 of DIMACS: Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, 1997.

• [PS] E. Allen Emerson. Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic Approach TOPLAS 19(4): 617-638, 1997.

• Edmund M. Clarke, E. Allen Emerson, Somesh Jha, A. Prasad Sistla: Symmetry Reductions in Model Checking. CAV 1998: 147-158

• E. Allen Emerson, Kedar S. Namjoshi: Verification of Parameterized Bus Arbitration Protocol. CAV 1998: 452-463

• E. Allen Emerson, Richard J. Trefler: Model Checking Real-Time Properties of Symmetric Systems. MFCS 1998: 427-436

• Anish Arora, Paul C. Attie, E. Allen Emerson: Synthesis of Fault-Tolerant Concurrent Programs. PODC 1998: 173-182

• Paul C. Attie, E. Allen Emerson: Synthesis of Concurrent Systems with Many Similar Processes. TOPLAS 20(1): 51-115 (1998)

• William Canfield, E. Allen Emerson, Avijit Saha: Checking Formal Specifications under Simulation. ICCD 1997: 455-460

• E. Allen Emerson, Somesh Jha, Doron Peled: Combining Partial Order and Symmetry Reductions. TACAS 1997: 19-34

• E. Allen Emerson, Richard J. Trefler: Generalized Quantitative Temporal Reasoning: An Automata Theoretic Approach. TAPSOFT 1997: 189-200

• E. Allen Emerson, A. Prasad Sistla: Utilizing Symmetry when Model-Checking under Fairness Assumptions: An Automata-Theoretic Approach. TOPLAS 19(4): 617-638 (1997)

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

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

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

• E. Allen Emerson, A. Prasad Sistla: Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic Approach. CAV 1995: 309-324

• E. Allen Emerson, Kedar S. Namjoshi: Reasoning about Rings. POPL 1995: 85-94

• E. Allen Emerson, Charanjit S. Jutla, A. Prasad Sistla: On Model-Checking for Fragments of 5-Calculus. CAV 1993: 385-396

• E. Allen Emerson, A. Prasad Sistla: Symmetry and Model Checking. CAV 1993: 463-478

• Farn Wang, Aloysius K. Mok, E. Allen Emerson: Distributed Real-Time System Specification and Verification in APTL. TOSEM 2(4): 346-378 (1993)

• Farn Wang, Aloysius K. Mok, E. Allen Emerson: Formal Specification of Ssynchronous Distributed Real-Time Systems by APTL. ICSE 1992: 188-198

• E. Allen Emerson, Tom Sadler, Jai Srinivasan: Efficient Temporal Satisfiability. Journal of Logic and Computation 2(2): 173-210 (1992)

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

• E. Allen Emerson: Real-Time and the Mu-Calculus (Preliminary Report). REX Workshop 1991: 176-194

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

• E. Allen Emerson, Jai Srinivasan: A Decidable Temporal Logic to Reason About Many Processes. PODC 1990: 233-246

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

• E. Allen Emerson, Tom Sadler, Jai Srinivasan: Efficient Temporal Reasoning. POPL 1989: 166-178

• Paul C. Attie, E. Allen Emerson: Synthesis of Concurrent Systems with Many Similar Sequential Processes. POPL 1989: 191-201

• Robert S. Streett, E. Allen Emerson: An Automata Theoretic Decision Procedure for the Propositional Mu-Calculus. Information and Computation 81(3): 249-264 (1989)

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

• E. Allen Emerson: Uniform Inevitability is Tree Automaton Ineffable. IPL 24(2): 77-79 (1987)

• E. Allen Emerson, Chin-Laung Lei: Modalities for Model Checking: Branching Time Logic Strikes Back. Science of Computer Programming 8(3): 275-306 (1987)

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

• E. Allen Emerson, Chin-Laung Lei: Temporal Reasoning Under Generalized Fairness Constraints. STACS 1986: 21-36

• E. Allen Emerson, Joseph Y. Halpern: ``Sometimes'' and ``Not Never'' Revisited: On Branching versus Linear Time Temporal Logic. JACM 33(1): 151-178 (1986)

• Edmund M. Clarke, E. Allen Emerson, A. Prasad Sistla: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. TOPLAS 8(2): 244-263 (1986)

• E. Allen Emerson, Chin-Laung Lei: Modalities for Model Checking: Branching Time Strikes Back. POPL 1985: 84-96

• E. Allen Emerson, Joseph Y. Halpern: Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. JCSS 30(1): 1-24 (1985)

• Robert S. Streett, E. Allen Emerson: The Propositional Mu-Calculus is Elementary. ICALP 1984: 465-472

• E. Allen Emerson, A. Prasad Sistla: Deciding Branching Time Logic. STOC 1984: 14-24

• E. Allen Emerson, A. Prasad Sistla: Deciding Full Branching Time Logic. Information and Control 61(3): 175-201 (1984)

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

• E. Allen Emerson, Joseph Y. Halpern: ``Sometimes'' and ``Not Never'' Revisited: On Branching Versus Linear Time. POPL 1983: 127-140

• E. Allen Emerson: Alternative Semantics for Temporal Logics. TCS 26: 121-130 (1983)

• E. Allen Emerson, Joseph Y. Halpern: Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. STOC 1982: 169-180

• E. Allen Emerson, Edmund M. Clarke: Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Science of Computer Programming 2(3): 241-266 (1982)

• E. Allen Emerson, Edmund M. Clarke: Characterizing Correctness Properties of Parallel Programs Using Fixpoints. ICALP 1980: 169-181

Technical Reports

Theses

Contact: trg@cs.utexas.edu