Efficient Coverability Analysis by Proof Minimization

We consider multi-threaded programs with an unbounded number of threads executing a finite-state, non-recursive procedure. Safety properties of such programs can be checked via reduction to the \emph{coverability problem} for well-structured transition systems (WSTS). We present a novel, sound and complete yet empirically much improved solution to this problem. The key idea to achieve a compact search structure is to track uncoverability only for minimal uncoverable elements, even if these elements are not part of the original coverability query. To this end, our algorithm examines elements in the downward closure of elements backward-reachable from the initial queries. A downside is that the algorithm may unnecessarily explore elements that turn out coverable and thus fail to contribute to the proof minimization. We counter this effect using a forward search engine that simultaneously generates (a subset of all) coverable elements, e.g., a generalised Karp-Miller procedure. We demonstrate in extensive experiments on C programs that our approach targeting minimal uncover ability proofs outperforms existing techniques by orders of magnitude.