Form Methods Syst Des DOI 10.1007/s10703-010-0096-7 Context-aware counter abstraction

Abstract The trend towards multi-core computing has made concurrent software an im-portant target of computer-aided verification. Unfortunately, Model Checkers for such soft-ware suffer tremendously from combinatorial state space explosion. We show how to ap-ply 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 im-plementations 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. We have carried out experiments on Boolean programs, an abstraction promoted by the success of the SLAM project. The ex-periments give evidence of the applicability of our method to realistic programs, and of the often huge savings obtained in comparison to plain symbolic state space exploration, and to exploration optimized by partial-order methods. To our knowledge, our tool marks the first implementation of counter abstraction to programs with non-trivial local state spaces, resulting in a Model Checker for concurrent Boolean programs that promises true scalability