Title: Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification,
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.