Abstract: We introduce an abstraction-based model checking method which relies on refinement of an under-approximation of the feasible behaviors of the system under analysis. The method preserves errors to safety properties, since all analyzed behaviors are feasible by definition. The method does not require an abstract transition relation to be generated, but instead executes the concrete transitions while storing abstract versions of the concrete states, as specified by a set of abstraction predicates. Two forms of refinement will be presented: based on weakest preconditions and symbolic forward execution. We will show how the technique complements traditional counter-example driven abstraction refinement.

In the second part of the presentation we discuss a lightweight variant of the method that can be used to do efficient testing. In particular we show a number of novel abstraction mappings that uses symbolic execution (including subsumption checking between states represented as symbolic constraints) that can be used to efficiently do test input generation for manipulating red-black trees in Java. We also compare this approach with a number of other test input generation strategies (classic model checking, random test selection, etc.).

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. After completion of his Ph.D. studies in October 1998 he 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 agents.