Richard J. Trefler

47 papers A* 6A 5B 13C 3Journal 8Unranked 12

Year	Rank	Type	Title / Venue / Authors
2025	A	`conf`	Relatively Complete and Efficient Partial Quantifier Elimination. CADE Estifanos Getachew, Arie Gurfinkel, Richard J. Trefler
2025	—	`conf`	Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications. VMCAI (2) Ruoxi Zhang, Richard J. Trefler, Kedar S. Namjoshi
2024	—	`conf`	Compositional Analysis of Parametric Cooperative Cyber-Physical Systems. FormaliSE@ICSE Raniah A. Alghamdi, Richard J. Trefler
2024	J	`jnl`	Inductive Predicate Synthesis Modulo Programs (Extended). CoRR Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
2024	A	`conf`	Inductive Predicate Synthesis Modulo Programs. ECOOP Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
2022	B	`conf`	Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications. FMCAD Ruoxi Zhang, Richard J. Trefler, Kedar S. Namjoshi
2022	B	`conf`	Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE. VMCAI Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
2021	J	`jnl`	Compositional Verification of Smart Contracts Through Communication Abstraction (Extended). CoRR Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
2021	B	`conf`	Compositional Verification of Smart Contracts Through Communication Abstraction. SAS Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
2019	—	`conf`	Local Reasoning for Parameterized First Order Protocols. NFM Rylo Ashmore, Arie Gurfinkel, Richard J. Trefler
2019	J	`jnl`	Local Reasoning for Parameterized First Order Protocols. CoRR Rylo Ashmore, Arie Gurfinkel, Richard J. Trefler
2019	J	`jnl`	Symmetry Reduction for the Local Mu-Calculus. CoRR Kedar S. Namjoshi, Richard J. Trefler
2018	—	`conf`	Symmetry Reduction for the Local Mu-Calculus. TACAS (2) Kedar S. Namjoshi, Richard J. Trefler
2016	A	`conf`	Parameterized Compositional Model Checking. TACAS Kedar S. Namjoshi, Richard J. Trefler
2015	A	`conf`	Analysis of Dynamic Process Networks. TACAS Kedar S. Namjoshi, Richard J. Trefler
2015	C	`conf`	Loop Freedom in AODVv2. FORTE Kedar S. Namjoshi, Richard J. Trefler
2013	B	`conf`	Uncovering Symmetries in Irregular Process Networks. VMCAI Kedar S. Namjoshi, Richard J. Trefler
2012	J	`jnl`	Explaining counterexamples using causality. Formal Methods Syst. Des. Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, Richard J. Trefler
2012	B	`conf`	Local Symmetry and Compositional Verification. VMCAI Kedar S. Namjoshi, Richard J. Trefler
2012	J	`jnl`	Reachability Problems in Piecewise FIFO Systems. ACM Trans. Comput. Log. Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, Richard J. Trefler
2011	—	`conf`	Symmetry for the Analysis of Dynamic Systems. NASA Formal Methods Zarrin Langari, Richard J. Trefler
2010	J	`jnl`	Model Checking Using Description Logic. J. Log. Comput. Shoham Ben-David, Richard J. Trefler, Grant E. Weddell
2010	J	`jnl`	On the completeness of compositional reasoning methods. ACM Trans. Comput. Log. Kedar S. Namjoshi, Richard J. Trefler
2009	B	`conf`	Application of Graph Transformation in Verification of Dynamic Systems. IFM Zarrin Langari, Richard J. Trefler
2009	A*	`conf`	Explaining Counterexamples Using Causality. CAV Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, Richard J. Trefler
2009	B	`conf`	Extending Symmetry Reduction by Exploiting System Architecture. VMCAI Richard J. Trefler, Thomas Wahl
2009	—	`conf`	Fair Cycle Detection using Description Logic Reasoning. Description Logics Shoham Ben-David, Jeffrey Pound, Richard J. Trefler, Dmitry Tsarkov, Grant E. Weddell
2009	—	`conf`	Verification of Parameterized Systems with Combinations of Abstract Domains. FMOODS/FORTE Naghmeh Ghafari, Arie Gurfinkel, Richard J. Trefler
2007	B	`conf`	Algorithmic Analysis of Piecewise FIFO Systems. FMCAD Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, Richard J. Trefler
2007	B	`conf`	Bounded Model Checking with Description Logic Reasoning. TABLEAUX Shoham Ben-David, Richard J. Trefler, Grant E. Weddell
2007	—	`conf`	Modal vs. Propositional Reasoning for model checking with Description Logics. Description Logics Shoham Ben-David, Richard J. Trefler, Grant E. Weddell
2006	B	`conf`	Formal Modeling of Communication Protocols by Graph Transformation. FM Zarrin Langari, Richard J. Trefler
2006	—	`conf`	Model checking the basic modalities of CTL with Description Logic. Description Logics Shoham Ben-David, Richard J. Trefler, Grant E. Weddell
2006	B	`conf`	Piecewise FIFO Channels Are Analyzable. VMCAI Naghmeh Ghafari, Richard J. Trefler
2006	C	`conf`	Reducing Model Checking of the Few to the One. ICFEM E. Allen Emerson, Richard J. Trefler, Thomas Wahl
2004	—	`conf`	Regularity Results for FIFO Channels. AVoCS Nils Klarlund, Richard J. Trefler
2003	A*	`conf`	A lattice-theoretic characterization of safety and liveness. PODC Panagiotis Manolios, Richard J. Trefler
2003	B	`conf`	Abstract Patterns of Compositional Reasoning. CONCUR Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler
2002	C	`conf`	Visual Specifications for Modular Reasoning about Asynchronous Systems. FORTE Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler
2001	A	`conf`	Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams. TACAS Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler
2001	A*	`conf`	Safety and Liveness in Branching Time. LICS Panagiotis Manolios, Richard J. Trefler
2000	A*	`conf`	On the Competeness of Compositional Reasoning. CAV Kedar S. Namjoshi, Richard J. Trefler
2000	A*	`conf`	Virtual Symmetry Reduction. LICS E. Allen Emerson, John Havlicek, Richard J. Trefler
1999	—	`conf`	From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking. CHARME E. Allen Emerson, Richard J. Trefler
1999	A*	`conf`	Parametric Quantitative Temporal Reasoning. LICS E. Allen Emerson, Richard J. Trefler
1998	B	`conf`	Model Checking Real-Time Properties of Symmetric Systems. MFCS E. Allen Emerson, Richard J. Trefler
1997	—	`conf`	Generalized Quantitative Temporal Reasoning: An Automata Theoretic Approach. TAPSOFT E. Allen Emerson, Richard J. Trefler