Thread Quantification for Concurrent Shape Analysis

In this paper, the authors address the problem of shape analysis for concurrent programs. They present new algorithms, based on abstract interpretation, for automatically verifying properties of programs with an unbounded number of threads manipulating an unbounded shared heap. Their algorithms are based on a new abstract domain whose elements represent thread-quantified invariants: i.e., invariants satisfied by all threads. They exploit existing abstractions to represent the invariants. Thus, their technique lifts existing abstractions by wrapping universal quantification around elements of the base abstract domain.