| 2004 |
|---|
| Paul C. Attie, Anish Arora, E. Allen Emerson. Synthesis of Fault-Tolerant Concurrent Programs. ACM TOPLAS. vol. 26. no. 1, Jan. 2004 125-185. ( postscript) |
| 2003 |
| E. Allen Emerson and Thomas Wahl. On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking. CHARME 2003: 216-230. ( postscript) |
| E. Allen Emerson and Kedar S. Namjoshi, On Reasoning about Rings, IJFCS (Special Issue on Verification and Analysis of Infinite State Systems), Vol. 14, No. 4, August 2003: 527-550 ( postscript) |
| E. Allen Emerson and Vineet Kahlon. Exact and Efficient Verification of Parameterized Cache Coherence Protocols. CHARME 2003: 247-262 ( postscript) |
| Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler: Abstract Patterns of Compositional Reasoning. CONCUR 2003: 423-438 ( postscript) |
| E. Allen Emerson, Vineet Kahlon: Model Checking Guarded Protocols. LICS 2003: 361-370 ( postscript) |
| E. Allen Emerson, Vineet Kahlon: Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols. TACAS 2003: 144-159 ( postscript) |
| 2002 |
| Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler: Visual Specifications for Modular Reasoning about Asynchronous Systems. FORTE 2002: 226-242 (Best Paper Award) ( postscript) |
| E. Allen Emerson, Vineet Kahlon: Model Checking Large-Scale and Parameterized Resource Allocation Systems. TACAS 2002: 251-265 ( postscript) |
| 2001 |
| Nina Amla, E. Allen Emerson, Kedar S. Namjoshi and Richard J. Trefler. Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams. TACAS 2001: Pages 465-479. (postscript ) |
| Nina Amla, E. Allen Emerson, Robert P. Kurshan, Kedar S. Namjoshi. RTDT: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams. CAV 2001: 387-390. ( postscript) |
| Paul C. Attie, E. Allen Emerson. Synthesis of concurrent programs for an atomic read/write model of computation. ACM Trans. Program. Lang. Syst. 23(2): 187-242 (2001). ( postscript) |
| E. Allen Emerson, Charanjit S. Jutla, A. Prasad Sistla. On model checking for the Mu-calculus and its fragments. Theor. Comput. Sci. 258(1-2): 491-522 (2001) ( postscript) |
| 2000 |
| E. Allen Emerson and Vineet Kahlon. Reducing Model Checking of the Many to the Few. CADE 2000: Pages 236-254. ( postscript) |
| Nina Amla, E. Allen Emerson, Robert P. Kurshan, and Kedar S. Namjoshi. Model Checking Synchronous Timing Diagrams. FMCAD 2000: Pages 283-298. ( postscript) |
| E. Allen Emerson. Model Checking: Theory into Practice. FSTTCS 2000: 1-10 ( postscript) |
| E. Allen Emerson, John Havlicek and Richard J. Trefler. Virtual Symmetry Reduction. LICS 2000: Pages 121-131 ( postscript) |
| A. Prasad Sistla, Viktor Gyuris and E. Allen Emerson. SMC: A Symmetry-based Model Checker for Verification of Safety and Liveness Properties. TOSEM 9(2): Pages 133-166 ( postscript) |
| 1999 |
| E. Allen Emerson and Richard J. Trefler. From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking. CHARME 1999: Pages 142-156. ( postscript) |
| Nina Amla, E. Allen Emerson and Kedar S. Namjoshi. Efficient Decompositional Model Checking for Regular Timing Diagrams. CHARME 1999: Pages 67-81. ( postscript) |
| E. Allen Emerson and Richard J. Trefler. Parametric Quantitative Temporal Reasoning. LICS 1999: Pages 336-343. ( postscript) |
| E. Allen Emerson and Charanjit S. Jutla. The Complexity of Tree Automata and Logics of Programs. SIAM J. Comput. 29(1): Pages 132-158 ( postscript) |
| 1998 |
| Edmund M. Clarke, E. Allen Emerson, Somesh Jha and A. Prasad Sistla. Symmetry Reductions in Model Checking. CAV 1998: Pages 147-158 ( postscript) |
| E. Allen Emerson and Kedar S. Namjoshi. Verification of Parameterized Bus Arbitration Protocol. CAV 1998: Pages 452-463. ( postscript) |
| E. Allen Emerson and Kedar S. Namjoshi. On Model Checking for Non-Deterministic Infinite-State Systems. LICS 1998: Pages 70-80. ( postscript) |
| E. Allen Emerson and Richard J. Trefler. Model Checking Real-Time Properties of Symmetric Systems. MFCS 1998: Pages 427-436. ( postscript) |
| Anish Arora, Paul C. Attie and E. Allen Emerson. Synthesis of Fault-Tolerant Concurrent Programs. PODC 1998: Pages 173-182. ( postscript) |
| Paul C. Attie and E. Allen Emerson: Synthesis of Concurrent Systems with Many Similar Processes. TOPLAS 20(1): Pages 51-115. ( postscript) |
| 1997 |
| William Canfield, E. Allen Emerson and Avijit Saha. Checking Formal Specifications under Simulation. ICCD 1997: Pages 455-460 ( postscript) |
| E. Allen Emerson, Somesh Jha and Doron Peled. Combining Partial Order and Symmetry Reductions. TACAS 1997: Pages 19-34. ( postscript) |
| E. Allen Emerson and Richard J. Trefler. Generalized Quantitative Temporal Reasoning: An Automata Theoretic Approach. TAPSOFT 1997: Pages 189-200. ( postscript) |
| E. Allen Emerson and A. Prasad Sistla. Utilizing Symmetry when Model-Checking under Fairness Assumptions: An Automata-Theoretic Approach. TOPLAS 19(4): Pages 617-638. ( postscript) |
| 1996 |
| E. Allen Emerson and Kedar S. Namjoshi. Automatic Verification of Parameterized Synchronous Systems (Extended Abstract). CAV 1996: Pages 87-98. ( postscript) |
| Paul C. Attie and E. Allen Emerson. Synthesis of Concurrent Systems for an Atomic Read / Atomic Write Model of Computation (Extended Abstract). PODC 1996: Pages 111-120. ( postscript) |
| Paul C. Attie, M. Singh, E.A. Emerson, A. Sheth, and M. Rusinkiewicz. Scheduling Workflows by Enforcing Intertask Dependencies. Distributed Systems Engineering Journal 3: Pages 222-238. ( gzipped postscript) |
| E. Allen Emerson and A. Prasad Sistla. Symmetry and Model Checking, Formal Methods in System Design 9(1/2) 1996: Pages 105-131. ( postscript) |
| 1995 |
| E. Allen Emerson and A. Prasad Sistla. Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic Approach. CAV 1995: Pages 309-324 |
| E. Allen Emerson and Kedar S. Namjoshi. Reasoning about Rings. POPL 1995: Pages 85-94. ( postscript) |
| 1993 |
| E. Allen Emerson, Charanjit S. Jutla and A. Prasad Sistla. On Model-Checking for Fragments of µ-Calculus. CAV 1993: Pages 385-396 |
| E. Allen Emerson and A. Prasad Sistla. Symmetry and Model Checking. CAV 1993: Pages 463-478 |
| Farn Wang, Aloysius K. Mok and E. Allen Emerson. Symbolic Model Checking for Distributed Real-Time Systems. FME 1993: Pages 632-651 |
| Farn Wang, Aloysius K. Mok and E. Allen Emerson. Distributed Real-Time System Specification and Verification in APTL. TOSEM 2(4): Pages 346-378 |
| 1992 |
| Farn Wang, Aloysius K. Mok and E. Allen Emerson. Formal Specification of Ssynchronous Distributed Real-Time Systems by APTL. ICSE 1992: Pages 188-198 |
| E. Allen Emerson, Tom Sadler and Jai Srinivasan. Efficient Temporal Satisfiability. Journal of Logic and Computation 2(2): Pages 173-210 |
| E. A. Emerson, A. K. Mok, A. P. Sistla, and J. Srinivasan. Quantitative Temporal Reasoning. Real Time Systems 4: Pages 331-352. ( postscript) |
| 1991 |
| E. Allen Emerson and Charanjit S. Jutla. Tree Automata, Mu-Calculus and Determinacy (Extended Abstract). FOCS 1991: Pages 368-377. ( postscript) |
| E. Allen Emerson: Real-Time and the Mu-Calculus (Preliminary Report). REX Workshop 1991: Pages 176-194 |
| 1990 |
| E. Allen Emerson, Michael Evangelist and Jai Srinivasan. On the Limits of Efficient Temporal Decidability (Extended Abstract). LICS 1990: Pages 464-475 |
| E. Allen Emerson and Jai Srinivasan. A Decidable Temporal Logic to Reason About Many Processes. PODC 1990: Pages 233-246 |
| 1989 |
| E. Allen Emerson and Charanjit S. Jutla. On Simultaneously Determinizing and Complementing omega-Automata (Extended Abstract). LICS 1989: Pages 333-342 |
| Allen Emerson, Tom Sadler and Jai Srinivasan. Efficient Temporal Reasoning. POPL 1989: Pages 166-178 |
| J. C. Browne, E. A. Emerson, M. G. Gouda, D. Miranker, A. K. Mok, and L. E. Rosier. Bounded-Time Fault-Tolerant Rule-Based Systems. Telematics and Informatics, 7(3/4) :Pages 441-454. |
| Paul C. Attie and E. Allen Emerson. Synthesis of Concurrent Systems with Many Similar Sequential Processes. POPL 1989: Pages 191-201 |
| Robert S. Streett and E. Allen Emerson. An Automata Theoretic Decision Procedure for the Propositional Mu-Calculus. Information and Computation 81(3): Pages 249-264 |
| 1988 |
| E. Allen Emerson and Charanjit S. Jutla. The Complexity of Tree Automata and Logics of Programs (Extended Abstract). FOCS 1988: pages 328-337 |
| E. Allen Emerson and Jai Srinivasan. Branching time temporal logic. REX Workshop 1988: Pages 123-172 |
| 1987 |
| E. Allen Emerson: Uniform Inevitability is Tree Automaton Ineffable. IPL 24(2): Pages 77-79 |
| E. Allen Emerson and Chin-Laung Lei. Modalities for Model Checking: Branching Time Logic Strikes Back. Science of Computer Programming 8(3): Pages 275-306 |
| 1986 |
| E. Allen Emerson and Chin-Laung Lei. Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract). LICS 1986: Pages 267-278 |
| E. Allen Emerson and Chin-Laung Lei. Temporal Reasoning Under Generalized Fairness Constraints. STACS 1986: Pages 21-36 |
| E. Allen Emerson and Joseph Y. Halpern. ``Sometimes'' and ``Not Never'' Revisited: On Branching versus Linear Time Temporal Logic. JACM 33(1): Pages 151-178 |
| Edmund M. Clarke, E. Allen Emerson and A. Prasad Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. TOPLAS 8(2): Pages 244-263 |
| 1985 |
| E. Allen Emerson and Chin-Laung Lei. Modalities for Model Checking: Branching Time Strikes Back. POPL 1985: Pages 84-96 |
| E. Allen Emerson and Joseph Y. Halpern. Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. JCSS 30(1): Pages 1-24 |
| E. Allen Emerson. Automata, Tableaux, and Temporal Logics. Conference on Logics of Programs. New York, NY. LNCS 193: Pages 79-88. |
| 1984 |
| Robert S. Streett and E. Allen Emerson. The Propositional Mu-Calculus is Elementary. ICALP 1984: Pages 465-472 |
| E. Allen Emerson and A. Prasad Sistla. Deciding Branching Time Logic. STOC 1984: Pages 14-24 |
| E. Allen Emerson and A. Prasad Sistla. Deciding Full Branching Time Logic. Information and Control 61(3): Pages 175-201 |
| 1983 |
| Edmund M. Clarke, E. Allen Emerson and A. Prasad Sistla. Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach. POPL 1983: Pages 117-126 |
| E. Allen Emerson and Joseph Y. Halpern. ``Sometimes'' and ``Not Never'' Revisited: On Branching Versus Linear Time. POPL 1983: Pages 127-140 |
| Allen Emerson. Alternative Semantics for Temporal Logics. TCS 26: Pages 121-130 |
| 1982 |
| E. Allen Emerson and Joseph Y. Halpern. Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. STOC 1982: Pages 169-180 |
| E. Allen Emerson and Edmund M. Clarke. Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Science of Computer Programming 2(3): Pages 241-266 |
| 1980 |
| E. Allen Emerson and Edmund M. Clarke. Characterizing Correctness Properties of Parallel Programs Using Fixpoints. ICALP 1980: Pages 169-181 |