Sciweavers

CAV
2009
Springer

Symbolic Counter Abstraction for Concurrent Software

14 years 4 months ago
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...
Daniel Kroening, Gérard Basler, Michele Maz
Added 25 Nov 2009
Updated 25 Nov 2009
Type Conference
Year 2009
Where CAV
Authors Daniel Kroening, Gérard Basler, Michele Mazzucchi, Thomas Wahl
Comments (0)