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

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

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)

On the Competeness of Compositional Reasoning. - Kedar S. Namjoshi; Richard J. Trefler (CAV, 2000)

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

Safety and Liveness in Branching Time. - Panagiotis Manolios; Richard J. Trefler (LICS, 2001)

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

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

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

A lattice-theoretic characterization of safety and liveness. - Panagiotis Manolios; Richard J. Trefler (PODC, 2003)

Regularity Results for FIFO Channels. - Nils Klarlund; Richard J. Trefler (AVoCS, 2004)

Model checking the basic modalities of CTL with Description Logic. - Shoham Ben-David; Richard J. Trefler; Grant E. Weddell (Description Logics, 2006)

Formal Modeling of Communication Protocols by Graph Transformation. - Zarrin Langari; Richard J. Trefler (FM, 2006)

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

Piecewise FIFO Channels Are Analyzable. - Naghmeh Ghafari; Richard J. Trefler (VMCAI, 2006)

Modal vs. Propositional Reasoning for model checking with Description Logics. - Shoham Ben-David; Richard J. Trefler; Grant E. Weddell (Description Logics, 2007)

Algorithmic Analysis of Piecewise FIFO Systems. - Naghmeh Ghafari; Arie Gurfinkel; Nils Klarlund; Richard J. Trefler (FMCAD, 2007)

Bounded Model Checking with Description Logic Reasoning. - Shoham Ben-David; Richard J. Trefler; Grant E. Weddell (TABLEAUX, 2007)

Fair Cycle Detection using Description Logic Reasoning. - Shoham Ben-David; Jeffrey Pound; Richard J. Trefler; Dmitry Tsarkov; Grant E. Weddell (Description Logics, 2009)

Verification of Parameterized Systems with Combinations of Abstract Domains. - Naghmeh Ghafari; Arie Gurfinkel; Richard J. Trefler (FMOODS/FORTE, 2009)

Application of Graph Transformation in Verification of Dynamic Systems. - Zarrin Langari; Richard J. Trefler (IFM, 2009)

Extending Symmetry Reduction by Exploiting System Architecture. - Richard J. Trefler; Thomas Wahl (VMCAI, 2009)

Model Checking Using Description Logic. - Shoham Ben-David; Richard J. Trefler; Grant E. Weddell (J. Log. Comput., 2010)

On the completeness of compositional reasoning methods. - Kedar S. Namjoshi; Richard J. Trefler (ACM Trans. Comput. Log., 2010)

Symmetry for the Analysis of Dynamic Systems. - Zarrin Langari; Richard J. Trefler (NASA Formal Methods, 2011)

Local Symmetry and Compositional Verification. - Kedar S. Namjoshi; Richard J. Trefler (VMCAI, 2012)

Explaining counterexamples using causality. - Ilan Beer; Shoham Ben-David; Hana Chockler; Avigail Orni; Richard J. Trefler (Formal Methods Syst. Des., 2012)

Reachability Problems in Piecewise FIFO Systems. - Naghmeh Ghafari; Arie Gurfinkel; Nils Klarlund; Richard J. Trefler (ACM Trans. Comput. Log., 2012)

Uncovering Symmetries in Irregular Process Networks. - Kedar S. Namjoshi; Richard J. Trefler (VMCAI, 2013)

Loop Freedom in AODVv2. - Kedar S. Namjoshi; Richard J. Trefler (FORTE, 2015)

Analysis of Dynamic Process Networks. - Kedar S. Namjoshi; Richard J. Trefler (TACAS, 2015)

Parameterized Compositional Model Checking. - Kedar S. Namjoshi; Richard J. Trefler (TACAS, 2016)

Symmetry Reduction for the Local Mu-Calculus. - Kedar S. Namjoshi; Richard J. Trefler (TACAS (2), 2018)

Local Reasoning for Parameterized First Order Protocols. - Rylo Ashmore; Arie Gurfinkel; Richard J. Trefler (NFM, 2019)

Compositional Verification of Smart Contracts Through Communication Abstraction. - Scott Wesley; Maria Christakis; Jorge A. Navas; Richard J. Trefler; Valentin Wüstholz; Arie Gurfinkel (SAS, 2021)

Compositional Verification of Smart Contracts Through Communication Abstraction (Extended). - Scott Wesley; Maria Christakis; Jorge A. Navas; Richard J. Trefler; Valentin Wüstholz; Arie Gurfinkel (CoRR, 2021)

Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications. - Ruoxi Zhang; Richard J. Trefler; Kedar S. Namjoshi (FMCAD, 2022)

Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE. - Scott Wesley; Maria Christakis; Jorge A. Navas; Richard J. Trefler; Valentin Wüstholz; Arie Gurfinkel (VMCAI, 2022)

Inductive Predicate Synthesis Modulo Programs. - Scott Wesley; Maria Christakis; Jorge A. Navas; Richard J. Trefler; Valentin Wüstholz; Arie Gurfinkel (ECOOP, 2024)

Compositional Analysis of Parametric Cooperative Cyber-Physical Systems. - Raniah A Alghamdi; Richard J. Trefler (FormaliSE@ICSE, 2024)

Inductive Predicate Synthesis Modulo Programs (Extended). - Scott Wesley; Maria Christakis; Jorge A. Navas; Richard J. Trefler; Valentin Wüstholz; Arie Gurfinkel (CoRR, 2024)

Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications. - Ruoxi Zhang; Richard J. Trefler; Kedar S. Namjoshi (VMCAI (2), 2025)