Richard Trefler
|
|
Teaching
CS 697 Fall 2024 --- under construction
CS 697 Schedule
Research
My research focuses on the application of automated reasoning tools, such as model checkers, to the analysis of reactive systems, including: computer hardware and software systems; embedded systems; and routing and communication protocols. Of particular interest are compositional reasoning and abstraction techniques for coping with the state explosion problem in model checking.
Additionally, I am interested in: visual notations for describing systems and their specifications; automata on infinite objects; temporal, modal, and description logics; Internet-based routing and communication protocols; and analysis of parameterized systems.
Selected Refereed Publications
Parameterized Compositional Model Checking
Kedar S. Namjoshi, Richard J. Trefler.
TACAS 2016: 589-606.
Loop Freedom in AODVv2
Kedar S. Namjoshi, Richard J. Trefler.
FORTE 2015: 98-112.
Analysis of Dynamic Process Networks
Kedar S. Namjoshi, Richard J. Trefler. TACAS 2015: 164-178.
Uncovering Symmetries in Irregular Process Networks
Kedar S. Namjoshi, Richard J. Trefler. VMCAI 2013:
496-514.
Explaining counterexamples using causality
Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, Richard
J. Trefler.
Formal Methods in System Design 40(1): 20-40 (2012)
Reachability Problems in Piecewise FIFO Systems
Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, Richard J. Trefler.
ACM Trans. Comput. Log. 13(1): 7:1-7:33 (2012)
Local Symmetry and Compositional Verification
Kedar S. Namjoshi, Richard J. Trefler. VMCAI 2012: 348-362.
Model Checking Using Description Logic
Shoham Ben-David, Richard Trefler and Grant Weddell.
To appear in the Journal of Logic and Computation, 28 pages.
On The Completeness of Compositional Reasoning Methods
Kedar Namjoshi and Richard Trefler. To appear in ACM Transactions on
Computational Logic, 20 pages.
A Semantic Characterization of Safety and Liveness for Branching Time Logics
Panagiotis Manolios and Richard Trefler. To appear in Distributed Computing, 21 pages.
Algorithmic Analysis of Piecewise FIFO Systems
Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, and Richard Trefler.
Formal Methods in Computer Aided Design, Nov. 2007, IEEE, 8 pages.
Bounded Model Checking with Description Logic Reasoning
Shoham Ben-David, Richard Trefler, and Grant Weddell.
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2007),
Lecture Notes in Computer Science, July 2007, 14 pages.
Modal vs. Propositional Reasoning for Model Checking with Description Logic
Shoham Ben-David, Richard Trefler, and Grant Weddell. 20th International Workshop
on Description Logics (DL'07), CEUR proceedings,
June 2007, 8 pages.
Reducing Model Checking of the Few to the One
E. Allen Emerson, Richard J. Trefler, and Thomas Wahl.
8th International Conference on Formal Engineering Methods, ICFEM 2006, Lecture Notes in
Computer Science 4260, 94-113.
Model Checking The Basic Modalities of CTL with Description Logic
Shoham Ben-David, Richard Trefler, and Grant Weddell.
19th International Workshop on Description Logics (DL'06), 2006, CEUR Proceedings vol. 189,
8 pages.
Formal Modeling of Communication Protocols by Graph Transformation
Zarrin Langari and Richard J. Trefler. Formal Methods 2006, 14th International
Symposium on Formal Methods, Lecture Notes in
Computer Science 4085, 348-363.
Piecewise FIFO Channels Are Analyzable
Naghmeh Ghafari and Richard J. Trefler.
Proceedings of the International Conference on
Verification, Model Checking, and Abstract Interpretation 2006,
Lecture Notes in Computer Science 3855, 252-266.
Regularity Results for FIFO Channels
Nis Klarlund and Richard Trefler. Automated Verifications of Critical Systems,
September, 2004. Electronic Notes in Theoretical
Computer Science, Vol. 128, number 6, Springer-Verlag, 2005, 15 pages.
A Lattice Theoretic Characterization of Safety and Liveness
Panagiotis Manolios and Richard Trefler.
ACM Symposium on Principles of Distributed Computing, 2003,
page 325-333.
Abstract Patterns of Compositional Reasoning
Nina Amla, E. Allen Emerson, Kedar Namjoshi and Richard Trefler
Conference on Concurrency Theory, Lecture Notes in Computer
Science 2761, 2003, pages 431-445.
Visual Specifications for Modular Reasoning
About Asynchronous Systems
Nina Amla, E. Allen Emerson,
Kedar Namjoshi and Richard Trefler. Received the Best Paper award at the
22nd IFIP FORTE Conference, Nov. 2002, pages 226-243.
Modular Timing Diagrams
Nina Amla, E. Allen Emerson, Kedar Namjoshi, and Richard J. Trefler. Proceedings of the
Cadence Technical Conference, 2002, 5 pages.
Safety and Liveness in Branching Time
Panagiotis Manolios and Richard Trefler.
16th Annual
IEEE Symposium on Logic in Computer
Science, IEEE, June, 2001, pages 366-374.
ECLIPSE Feature Logic Analysis
Gregory Bond, Franjo Ivancic,
Nils Klarlund and Richard Trefler.
Second IP Telephony Workshop, April 2001, 8 pages.
Assume-Guarantee Based Compositional
Reasoning for Timing Diagrams
Nina Amla, E. Allen Emerson, Kedar Namjoshi and Richard Trefler.
Tools and Algorithms
for the Correctness and Analysis of Systems Conference, part of ETAPS,
LNCS 2031, April 2001, pages 265-279.
On The Completeness of Compositional Reasoning
Kedar Namjoshi and Richard Trefler. 12th International
Conference on Computer Aided Verification, LNCS 1855,
July, 2000, pages 435-449.
Virtual Symmetry Reduction
E. Allen Emerson,
John Havlicek and Richard Trefler.
15th Annual
IEEE Symposium on Logic in Computer
Science, June, 2000, pages 121-131.
From Asymmetry to Full Symmetry: New Techniques
for Symmetry Reduction in Model Checking
E. Allen Emerson and Richard Trefler. CHARME99: 10th
IFIP WG10.5 Advanced Research Working Conference on Correct
Hardware Design and Verification Methods, Springer
1999, pages 142-156.
Parametric Quantitative Temporal Reasoning
E. Allen Emerson and Richard Trefler.
14th Annual IEEE
Symposium on Logic in Computer
Science, IEEE, 1999, pages 336-343.
Model Checking Real-Time Properties of Symmetric
Systems
E. Allen Emerson and Richard Trefler.
23rd International Symposium on the
Mathematical Foundations of Computer Science,
LNCS 1450, 1998, pages 427-436.
Generalized Quantitative Temporal Reasoning: An
Automata-Theoretic
Approach
E. Allen Emerson and Richard Trefler.
TAPSOFT'97: Theory
and Practice of Software Development
Springer-Verlag,
LNCS 1214, 1997, pages 189-200.
Current Students
Ruoxi Zhang
Former Students
Zarrin Langari, Ph.D. 2011.
Shoham Ben-David, Ph.D. 2009.
Naghmeh Ghafari, Ph.D. 2009.
Jane D. Thi Tang, M. Math. 2006.
Contact information
Postal Address
School of Computer Science trefler at uwaterloo.ca |
Telephone
Office: OfficeDC |