## Thread-modular Abstraction Refinement

*
Thomas A. Henzinger,
Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer*

We present an algorithm called TAR ("Thread-modular Abstraction
Refinement") for model checking safety properties of concurrent
software. The TAR algorithm uses thread-modular assume-guarantee
reasoning to overcome the exponential complexity in the control state
of multithreaded programs. Thread modularity means that TAR explores
the state space of one thread at a time, making assumptions about how
the environment can interfere. The TAR algorithm uses
counterexample-guided predicate-abstraction refinement to overcome the
usually infinite complexity in the data state of C programs. A
successive approximation scheme automatically infers the necessary
precision on data variables as well as suitable environment
assumptions. The scheme is novel in that transition relations are
approximated from above, while at the same time environment
assumptions are approximated from below. In our software verification
tool *Blast* we have implemented a fully automatic race checker
for multithreaded C programs which is based on the TAR algorithm.
This tool has verified a wide variety of commonly used locking idioms,
including locking schemes that are not amenable to existing dynamic
and static race checkers such as *Eraser* or *Warlock*.

*Proceedings of the
15th International Conference on Computer-Aided Verification*
(CAV),
Lecture Notes in Computer Science 2725,
Springer, 2003, pp. 262-274.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2003 Springer.