Abstract We consider the use of commutativity-based reduction for the algorithmic verification of concurrent programs. In existing work, the commutativity relation used for the reduction is mostly fixed statically. In this paper, we propose a demand-driven approach to compute the commutativity relation. The approach can be viewed as the direct analogue of the CEGAR approach which uses counterexamples to guide the incremental refinement of the abstraction. Instead of eliminating a counterexample by proving it infeasible and refining the abstraction, we can eliminate a counterexample by proving it redundant and expanding the commutativity relation. When we prove a counterexample redundant, we use the proof for a generalization step which allows us to eliminate not just a single counterexample, but a whole infinite set. We present a general scheme where we integrate the new approach with the CEGAR approach. We have implemented an instantiation of the general scheme. An experimental evaluation shows an increase in the number of successfully verified programs by 15% on a challenging benchmark set.

Abstract Ultimate GemCutter verifies concurrent programs using the CEGAR paradigm, by generalizing from spurious counterexample traces to larger sets of correct traces. We integrate classical CEGAR generalization with orthogonal generalization across interleavings. Thereby, we are able to prove correctness of programs otherwise out-of-reach for interpolation-based verification. The competition results show significant advantages over other concurrency approaches in the Ultimate family.