| 2025 | CADE | Relatively Complete and Efficient Partial Quantifier Elimination. | Estifanos Getachew, Arie Gurfinkel, Richard J. Trefler |
| 2025 | VMCAI | Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications. | Ruoxi Zhang, Richard J. Trefler, Kedar S. Namjoshi |
| 2024 | ECOOP | Inductive Predicate Synthesis Modulo Programs. | Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wstholz, Arie Gurfinkel |
| 2022 | FMCAD | Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications. | Ruoxi Zhang, Richard J. Trefler, Kedar S. Namjoshi |
| 2022 | VMCAI | Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE. | Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wstholz, Arie Gurfinkel |
| 2021 | SAS | Compositional Verification of Smart Contracts Through Communication Abstraction. | Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wstholz, Arie Gurfinkel |
| 2018 | TACAS | Symmetry Reduction for the Local Mu-Calculus. | Kedar S. Namjoshi, Richard J. Trefler |
| 2016 | TACAS | Parameterized Compositional Model Checking. | Kedar S. Namjoshi, Richard J. Trefler |
| 2015 | FORTE | Loop Freedom in AODVv2. | Kedar S. Namjoshi, Richard J. Trefler |
| 2015 | TACAS | Analysis of Dynamic Process Networks. | Kedar S. Namjoshi, Richard J. Trefler |
| 2013 | VMCAI | Uncovering Symmetries in Irregular Process Networks. | Kedar S. Namjoshi, Richard J. Trefler |
| 2012 | VMCAI | Local Symmetry and Compositional Verification. | Kedar S. Namjoshi, Richard J. Trefler |
| 2009 | CAV | Explaining Counterexamples Using Causality. | Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, Richard J. Trefler |
| 2009 | FORTE | Verification of Parameterized Systems with Combinations of Abstract Domains. | Naghmeh Ghafari, Arie Gurfinkel, Richard J. Trefler |
| 2009 | IFM | Application of Graph Transformation in Verification of Dynamic Systems. | Zarrin Langari, Richard J. Trefler |
| 2009 | VMCAI | Extending Symmetry Reduction by Exploiting System Architecture. | Richard J. Trefler, Thomas Wahl |
| 2007 | FMCAD | Algorithmic Analysis of Piecewise FIFO Systems. | Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, Richard J. Trefler |
| 2007 | TABLEAUX | Bounded Model Checking with Description Logic Reasoning. | Shoham Ben-David, Richard J. Trefler, Grant E. Weddell |
| 2006 | FM | Formal Modeling of Communication Protocols by Graph Transformation. | Zarrin Langari, Richard J. Trefler |
| 2006 | ICFEM | Reducing Model Checking of the Few to the One. | E. Allen Emerson, Richard J. Trefler, Thomas Wahl |
| 2006 | VMCAI | Piecewise FIFO Channels Are Analyzable. | Naghmeh Ghafari, Richard J. Trefler |
| 2003 | CONCUR | Abstract Patterns of Compositional Reasoning. | Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler |
| 2003 | PODC | A lattice-theoretic characterization of safety and liveness. | Panagiotis Manolios, Richard J. Trefler |
| 2002 | FORTE | Visual Specifications for Modular Reasoning about Asynchronous Systems. | Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler |
| 2001 | LICS | Safety and Liveness in Branching Time. | Panagiotis Manolios, Richard J. Trefler |
| 2001 | TACAS | Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams. | Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler |
| 2000 | CAV | On the Competeness of Compositional Reasoning. | Kedar S. Namjoshi, Richard J. Trefler |
| 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 | MFCS | Model Checking Real-Time Properties of Symmetric Systems. | E. Allen Emerson, Richard J. Trefler |