Symbolic Counter Abstraction for Concurrent Software

November 13, 2009
Daniel Kroening | Oxford University

The trend towards multi-core computing has made concurrent software an important target of computer-aided verification. Unfortunately, Model Checkers for such software suffer tremendously from combinatorial state space explosion. We show how to apply counter abstraction to real-world concurrent programs to factor out redundancy due to thread replication. The traditional global state representation as a vector of local states is replaced by a vector of thread counters, one per local state. In practice, straightforward implementations of this idea are unfavorably sensitive to the number of local states. We present a novel symbolic exploration algorithm that avoids this problem by carefully scheduling which counters to track at any moment during the search. Our experiments are carried out on Boolean programs, an abstraction promoted by the SLAM project. To our knowledge, this marks the first application of counter abstraction to programs with non-trivial local state spaces, and results in the first scalable Model Checker for concurrent Boolean programs.

Speaker Details

Daniel Kroening received the M.E. and doctoral degrees in computer science from the University of Saarland, Saarbruecken, in 1999 and 2001, respectively. He joined the Model Checking group in the Computer Science Department at Carnegie Mellon University, Pittsburgh PA, USA, in 2001 as a Post-Doc.He was an assistant professor at the Swiss Technical Institute (ETH) in Zurich, Switzerland, from 2004 to 2007. He is now a Reader at the Computing Laboratory at Oxford University. His research interests include automated formal verification of hardware and software systems, decision procedures, with a focus on the verification of large-scale industrial systems given in C or C++.