Invited Talks and Tutorials

We propose to build model checkers as flexible components that can be composed to new, complementing, more powerful verifiers. Classical model checkers take as input a model and a specification, and have three possible outcomes:

• (1) the model satisfies the specification,
• (2) the model does not satisfy the specification,
• (3) the model checker fails.

The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported.

Conditional model checking always reports a summary of the performed work even if it is not able to report complete verification. A conditional model checker takes as input a model and a specification, and returns a condition P ---usually a state predicate--- such that the program satisfies the specification under the condition P --- that is, as long as the program does not leave the states in which P is satisfied.

This new view on model checking enables many practical and important applications. Most importantly, conditional model checkers can be used to solve verification problems in a compositional manner.

One example is the sequential combination of model checkers with information passing. We can give the condition that one model checker produces, as input to a second conditional model checker, such that the verification problem for the second is restricted to the part of the state space that is not covered by the condition, i.e., the second model checker works on the problems that the first model checker could not solve.

Dirk Beyer is Professor of Computer Science at the University of Passau, Germany and Adjunct Professor in the School of Computing Science at Simon Fraser University, B.C., Canada. He holds a Dipl.-Inf. degree (1998) and a Dr. rer. nat. degree (2002) in Computer Science from the Brandenburg University of Technology in Cottbus, Germany. He was Postdoctoral Researcher in the School of Computer and Communication Sciences at EPFL in Lausanne, Switzerland (2004-2006), and in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley, U.S.A. (2003-2004). In 1998 he was Software Engineer with Siemens AG, SBS Dept. Major Projects in Dresden, Germany. His research focuses on models, algorithms, and tools for the construction and analysis of reliable software systems. He is the architect, designer, and implementor of several successful tools, for example, CrocoPat is the first efficient interpreter for relational programming, CCVisu is a successful tool for visual clustering, and CPAchecker and BLAST are two of the most successful software model checkers. He is a member of the ACM, the IEEE, and the IEEE Computer Society.

How do you prove the correctness of a concurrent algorithm? This question has been asked since at least the mid-sixties. It has inspired researchers ever since, and it has produced a broad range of tentative solutions. Many of these solutions are based on mathematical theories, program annotations, or the construction of abstract models.

What we ultimately want, though, is a basic tool that we can point at an arbitrary piece of C code, and that can answer queries about the validity of interesting properties of that code.

We may be very close to a solution to this decades old problem. In this tutorial we will describe a method that makes use of a model extractor that interfaces smoothly with the Spin model checker to verify automatically generated models of arbitrary multi-threaded code written in C.

The model extractor requires minimal user interaction for basic applications, but also allows more advanced users to define powerful abstractions, to support the verification of larger problems. Examples of the use of this method include the formal verification of mission-critical software for interplanetary spacecraft.