Dynamic reductions for model checking concurrent software
From MaRDI portal
Publication:2961569
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.
Recommendations
- Dynamic partial-order reduction for model checking software
- Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions
- Peephole Partial Order Reduction
- Space-reduction strategies for model checking dynamic software
- Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
Cites work
- scientific article; zbMATH DE number 3986679 (Why is no real title available?)
- scientific article; zbMATH DE number 42752 (Why is no real title available?)
- scientific article; zbMATH DE number 1956603 (Why is no real title available?)
- A calculus of atomic actions
- An efficient partial order reduction algorithm with an alternative proviso implementation
- Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
- Dynamic partial-order reduction for model checking software
- Dynamic reductions for model checking concurrent software
- Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs
- Graph theory with applications
- Lazy Abstraction with Interpolants
- Lazy abstraction
- Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
- Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
- Partial-order reduction in symbolic state-space exploration
- Peephole Partial Order Reduction
- Proof-guided underapproximation-widening for multi-process systems
- Reduction
- SAT-Based Model Checking without Unrolling
- Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions
- Transactions for software model checking
Cited in
(11)- Dynamic Path Reduction for Software Model Checking
- scientific article; zbMATH DE number 1744960 (Why is no real title available?)
- Ant colony optimization with partial order reduction for discovering safety property violations in concurrent models
- Space-reduction strategies for model checking dynamic software
- Dynamic partial-order reduction for model checking software
- Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions
- Dynamic reductions for model checking concurrent software
- Peephole Partial Order Reduction
- Model Checking Software
- Correct Hardware Design and Verification Methods
- A model reduction method for parallel software testing
This page was built for publication: Dynamic reductions for model checking concurrent software
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2961569)
