Dynamic Reductions for Model Checking Concurrent Software

TL;DR

This paper introduces a dynamic reduction method for symbolic model checking of concurrent software, reducing interleavings efficiently by extending bisimilarity and dynamic transactions, leading to improved verification performance.

Contribution

It extends Lipton's reduction with bisimilarity and dynamic transactions, enabling more effective and less analysis-dependent reduction in symbolic model checking.

Findings

Effective reduction of interleavings demonstrated on case studies.

Implementation of the method in IC3 and BMC shows practical efficiency.

Significant performance improvements on SVCOMP benchmarks.

Abstract

Symbolic model checking of parallel programs stands and falls with effective methods of dealing with the explosion of interleavings. We propose a dynamic reduction technique to avoid unnecessary interleavings. By extending Lipton's original work with a notion of bisimilarity, we accommodate dynamic transactions, and thereby reduce dependence on the accuracy of static analysis, which is a severe bottleneck in other reduction techniques. The combination of symbolic model checking and dynamic reduction techniques has proven to be challenging in the past. Our generic reduction theorem nonetheless enables us to derive an efficient symbolic encoding, which we implemented for IC3 and BMC. The experiments demonstrate the power of dynamic reduction on several case studies and a large set of SVCOMP benchmarks.