Computing That Serves

Combining Model Checking and Symbolic Execution


Thursday, February 5, 2004 - 10:00am


Dr. Willem Visser, NASA Ames Research Center

The talk will consist of three parts: a brief introduction to the Java PathFinder (JPF) model checker and some of its more novel features, symbolic execution as implemented in JPF, and how the latter is used to do invariant generation, predicate abstraction and test-input generation. The introduction to JPF will include a description of the general architecture as well as examples of the tool's usage. The symbolic execution within JPF is novel since it supports both the more traditional constraint solving over (linear) integer constraints as well as structural constraints for arrays, linked lists, red-black trees, etc. The main part of the talk will focus on the usage of the symbolic execution within JPF. It will be shown how loop termination is treated by invariant generation and predicate abstraction based approaches. Lastly, JPF's capabilities as a test-input generation tool will be highlighted by showing how it can be used to cover all branches in the code for manipulating red-black trees.


Willem Visser received his Ph.D. from the University of Manchester in 1998. His thesis introduced the first efficient automata-theoretic algorithm for model checking CTL* properties. Prior to his PhD he received an M.Sc from the University of Stellenbosch (South Africa) for his work on the development of a model checker for operating system kernels. After completion of his Ph.D. studies he taught a course on model checking at the University of Stellenbosch for 3 months and in October 1998 started work at the Research Institute for Advanced Computer Science (RIACS) at NASA Ames. His main research focus is on the application of model checking to programming languages. To this end he has been the main developer of the Java PathFinder model checker for Java - that won the 2003 TGIR Engineering Innovation award from the Office of Aerospace Technology at NASA. This model checker is the first model checker that is custom-made for the Java language. His current work focuses on using symbolic execution and model checking for test-case generation and program proofs, environment generation, feasible counter-example detection during abstraction-based model checking, belief-logics and agent verification.