Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification

TL;DR

This paper introduces a novel abstraction refinement technique for multi-threaded program verification that reduces complexity by focusing on scheduling constraints, leading to more efficient bounded model checking.

Contribution

It proposes a scheduling constraint-based abstraction refinement method that avoids complex encodings and introduces graph-based algorithms for effective counterexample validation and refinement.

Findings

Significantly outperforms existing tools on SV-COMP benchmarks.

Proves soundness and completeness for given loop unwinding depth.

Reduces formula complexity by focusing on scheduling constraints.

Abstract

Bounded model checking is among the most efficient techniques for the automatic verification of concurrent programs. However, encoding all possible interleavings often requires a huge and complex formula, which significantly limits the salability. This paper proposes a novel and efficient abstraction refinement method for multi-threaded program verification. Observing that the huge formula is usually dominated by the exact encoding of the scheduling constraint, this paper proposes a \tsc based abstraction refinement method, which avoids the huge and complex encoding of BMC. In addition, to obtain an effective refinement, we have devised two graph-based algorithms over event order graph for counterexample validation and refinement generation, which can always obtain a small yet effective refinement constraint. Enhanced by two constraint-based algorithms for counterexample validation and refinement generation, we have proved that our method is sound and complete w.r.t. the given loop unwinding depth. Experimental results on \svcompc benchmarks indicate that our method is promising and significantly outperforms the existing state-of-the-art tools.