Associate Professor
Joined School 2002
BA (University of Toronto),
MSc (University of Texas at Austin),
PhD (University of Texas at Austin)
| trefler@uwaterloo.ca | |
| Web | http://se.uwaterloo.ca/~trefler |
| Voice | 519-888-4567 x37508 |
| Fax | 519-885-1208 |
|
| Richard Trefler
Associate Professor Joined School 2002 BA (University of Toronto),
|
Computer hardware, software, and embedded systems are growing ever larger and more complex, and these facts mitigate against completely error-free, predictable operation. Yet these very systems are deployed in areas from network communications to avionics where reliability is critical, and errors are both damaging and costly.
Professor Trefler works on developing tools for the automated analysis of computer systems. In particular, his focus is on improving the applicability of precise mathematical tools known as model checkers, to both error detection and verification of general classes of computer systems.
Model checking is successfully used in the analysis of many large safety critical systems. However, model checking confronts one important limitation known as the state explosion problem -- systems have short textual descriptions that can result in potentially enormous state spaces that the model checkers must analyze.
Professor Trefler's has recently shown how to generalize abstraction techniques based on system symmetry for the purpose of reducing the size of systems under analysis. Abstraction techniques are useful in model checking since they allow large systems to be replaced by much smaller, more tractably sized systems that are equivalent for the purposes of finding bugs and proving system correctness. Symmetry reduction techniques are applicable to systems composed of many replicated components. Ideally, these techniques reduce the number of systems states needed to be analyzed by grouping together sets of states that are symmetric to each other. This recent work has shown that by generalizing the notion of system symmetry to capture the architecture used in systems design, symmetry reduction techniques can be applied to systems designs, such as rings and tori, that were not previously amenable to symmetry reduction.
Compositional reasoning, where one reasons about individual processes in order to analyze multi-component systems is another technique Professor Trefler has used in his research on mitigating state explosion in model checking. This style of reasoning is typically based on an assume-guarantee paradigm. That is, one tries to show that both a system and its components behave correctly under the assumptions that the inputs to the components are the expected ones. Mathematically precise compositional reasoning rules that encode the mathematical requirements needed to perform such reasoning can be delicate, as some are syntactically circular in nature, in that assumptions and guarantees are mutually dependent. This is known to be a source of unsoundness. In Professor's Trefler's recent article, he investigated rules for compositional reasoning from the viewpoint of completeness. He showed that several existing rules are incomplete: that is, there are properties whose validity cannot be established using (only) these rules. He then derived a new, circular, reasoning rule and showed it to be sound and complete. He was also able to show that the auxiliary assertions needed for completeness may be defined only on the interface of the component processes. He was also able to show that the two main paradigms of circular and noncircular reasoning are closely related, in that a proof of one type can be transformed in a straightforward manner to one of the other type. These results give some insight into the applicability of compositional reasoning methods and related work by Professor Trefler has used these techniques in the analysis of communication protocols.
Professor Trefler is also interested in the study of mathematically precise, visual notations for describing and analyzing the behaviour of reactive protocols. His recent work has shown that visual, graph transformation based modelling languages may play an important role in analyzing the various features of communication protocols.
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.
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.
David R. Cheriton School of Computer Science
University of Waterloo
Waterloo, Ontario, Canada N2L 3G1
Tel: 519-888-4567 x33293
Fax: 519-885-1208
Contact | Feedback: cs-webmaster@cs.uwaterloo.ca | David R. Cheriton School of Computer Science | Faculty of Mathematics
Last modified: Thursday, 13-Jan-2011 13:54:54 EST
