THIS SITE

Information for

Richard Trefler

Professor

Richard TreflerResearch interests

Automated Analysis of Reactive Systems, Model Checking, Temporal Logic, Systems Specifications, Compositional Reasoning, Symmetry Reduction Hardware, software, and embedded systems are growing ever larger and more complex, and they are deployed all around us -- from network communications to cars to medical devices and avionics. Reliability is critical, errors are damaging and costly -- yet completely error-free, predictable operation is getting ever more challenging. How can we assure ourselves that these systems will operate as intended?

I work on developing tools for the automated analysis of reactive systems -- those computer hardware, software or embedded systems that interact with an environment over which they have little or no control.

In particular, my research aims to improve the applicability of mathematically rigorous tools, called model checkers, to both error detection and verification of general classes of computer systems.

Model checking is a very successful approach that is widely used to analyze many safety or business critical systems. However, it confronts one important limitation known as the state explosion problem -- systems (or programs) have relatively short textual descriptions that can result in potentially enormous state spaces that must be analyzed. Much of my research aims to find ways to mitigate state explosion and thereby extend the applicability of model checking. In particular, I have developed new approaches to symmetry reduction and compositional reasoning.

Symmetry reduction takes advantage of similarities between components to reduce the number of components needing to be analyzed. Compositional reasoning techniques break up systems of many components so each can be analyzed in isolation. With my collaborators and students, I have achieved several key results in these areas.

Recently, I have been looking at parametrized systems of multiple components operating on many different network topologies, or even changing topologies, such as routing or communications protocols. I am developing several novel approaches to analyze this challenging but important class of systems.

In general, my research is done collaboratively, with my students and colleagues at UW, and with collaborators at the University of Texas at Austin and Alcatel-Lucent Bell-Labs, among others.

Degrees and awards

BA (Toronto), MSc, PhD (Texas, Austin)

Industrial and sabbatical experience

From 1999 to 2002 Professor Trefler was a senior member of technical staff at AT&T Labs - Research in Florham Park, New Jersey. He worked on the application of automated reasoning tools to the development of reliable software communications systems and in particular to Internet based telephony systems.

In 2006 Professor Trefler was an invited speaker and guest scientist at the 2006 Logic and Algorithms Programme at the Isaac Newton Institute for the Mathematical Sciences, Cambridge University, Cambridge, in the United Kingdom.

He and his co-authors won the Best Paper Award at the 2002 IFIP International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), for their work: Visual Specifications for Modular Reasoning About Asynchronous Systems.

In addition, Professor Trefler and his co-authors won the Best Paper Award at the 2002 Cadence Technical Conference for their work: Modular Timing Diagrams.

In the summer of 1998 and during his PhD studies Professor Trefler was invited to be a guest scientist at Siemens Corporate Technology in Munich, Germany. He developed model checking tools based on abstraction methods and investigated their applicability to hardware and software systems being developed at Siemens.

Representative publications

K. Namjoshi and Richard Trefler. On the Completeness of Compositional Reasoning Systems. ACM Transactions on Computational Logic (TOCL) Volume 11, Issue 3 (May 2010), Article No.: 16.

Richard J. Trefler and Thomas Wahl. Extending Symmetry Reduction by Exploiting System Architecture. "International Conference on Verification Model Checking and Abstract Interpretation (VMCAI), 320-334, 2009.

Naghmeh Ghafari, Arie Gurfinkel, Nils Klarland and Richard Trefler. Algorithmic Analysis of Piecewise FIFO Systems. "Formal Methods in Computer Aided Design (FMCAD 2007), Nov. 2007, IEEE, 8 pages.

Shoham Ben-David, Richard Trefler and Grant Weddell. Bounded Model Checking with Description Logic Reasoning. Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2007), Lecture Notes in Computer Science, 14 pages, 2007.

Naghmeh Ghafari, Arie Gurfinkel, Nils Klarland and Richard Trefler. Algorithmic Analysis of Piecewise FIFO Systems. "Formal Methods in Computer Aided Design (FMCAD 2007), Nov. 2007, IEEE, 8 pages.

Zarrin Langari and Richard Trefler. Formal Modeling of Communication Protocols by Graph Transformation. 14th International Symposium on Formal Methods, Lecture Notes in Computer Science 4085, 348-363, 2006.

N. Amla, E. A. Emerson, K. S. Namjoshi, and R. Trefler, Visual Specifications for Modular Reasoning about Asynchronous Systems. Received the Best Paper Award at the 22nd IFIP TC6 WG 6.1 Joint International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), LNCS 2529, pp. 226-242, 2002.

N. Amla, E. A. Emerson, K. S. Namjoshi, and R. Trefler. Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams. Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 2031, pp. 465-479, 2001.

P. Manolios and R. Trefler. Safety and Liveness in Branching Time. Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS), IEEE Press, pp. 366-374, 2001.

E. A. Emerson and R. Trefler. From Asymmetry to Full Symmetry New Techniques for Symmetry Reduction in Model Checking. Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), LNCS 1703, pp. 142-156, 1999.

Affiliation: 
University of Waterloo
Contact information: