Symbolic Counter Abstraction for Concurrent Software

Counter Abstraction for Concurrent Software G?erard Basler1 , Michele Mazzucchi1 , Thomas Wahl1,2 , Daniel Kroening1,2 1 Computer Systems Institute, ETH Zurich, Switzerland 2 Computing Laboratory, Oxford University, United Kingdom Abstract. 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 se...

• Type: Conference
• Year: 2009
• Where: CAV
• Authors: Daniel Kroening, Gérard Basler, Michele Mazzucchi, Thomas Wahl
• Keywords: CAV 2009, Concurrent Boolean Programs, Counter Abstraction, Formal Methods, Real-world Concurrent Programs