Warning: This website is no longer maintained, as I have left ETH Zurich for Oxford University. Please visit my new homepage.
Thomas Wahl
| Swiss Federal
Institute of Technology (Eidgenössische Technische Hochschule---ETH) Computer Systems Institute Department of Computer Science ETH Zentrum, RZ H6 Clausiusstrasse 59 CH-8092 Zürich Switzerland Phone: +41 44 63 23087 |
| Oxford
University Computing Lab Wolfson Building Parks Road Oxford, OX1 3QD United Kingdom Phone: +44 1865 610708 |
Welcome to my homepage. I am a Postdoctoral Researcher, working in the Formal Verification group led by Daniel Kröning (which is split between the Computer Science departments of ETH Zurich and of the University of Oxford). I completed the Ph.D. program at the Computer Sciences department at the University of Texas at Austin in 2007, under the supervision of E. A. Emerson.
Model Checking, co-invented by my dissertation supervisor, E. A. Emerson, is an algorithmic formal verification technique to exhaustively search the state space of systems representable by a finite-state model. Its main strengths are that, at least in principle, it is fully automatic (meaning that no user interaction is required during the verification process), that it is capable of processing complex queries of the system (not just reachability of an error state), and that in many cases it can provide evidence explaining why a property is true or false (for example, a trace showing how an alleged "bug" can be reached). Especially the latter property has led to successful applications of the technique in hardware and, to a lesser extent, software verification.
But there is also a major drawback: The exhaustive search of large state spaces often entails unsatisfiable memory and time requirements on computers running model checking algorithms. This central impediment to more widespread employment of the technique is known as the state space explosion problem. Tackling it is what model checking research today is mostly about, and mine is not an exception.
My approach is to exploit regularity that many systems exhibit, often due to the fact that custom-designed units are replicated into multiple instances that form the whole system. Examples include protocols governing the behavior of a large number of "identical" (for verification purposes) processes, homogeneous computer networks, or micro processors with memory arrays consisting of many identical cells. The key to exploiting this kind of regularity is that at an abstract level, such systems can often be described in a much more compact way than a complete transition system such as a Kripke structure. If the regularity is recognized at this level, we may be able to avoid the complexity due to replication altogether.
You can download my dissertation from a link in the "Book Chapter, Reports, Theses" section of this homepage.