Dynamic reductions for model checking concurrent software

DOI10.1007/978-3-319-52234-0_14zbMATH Open1484.68102arXiv1611.09318OpenAlexW2551596431MaRDI QIDQ2961569FDOQ2961569

Authors: Henning Günther, Alfons W. Laarman, Ana Sokolova, Georg Weissenbacher 

Publication date: 21 February 2017

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1611.09318

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Cites Work

• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Graph theory with applications
• Title not available (Why is that?)
• Dynamic partial-order reduction for model checking software
• SAT-Based Model Checking without Unrolling
• Title not available (Why is that?)
• Lazy Abstraction with Interpolants
• Lazy abstraction
• Transactions for software model checking
• Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
• Peephole Partial Order Reduction
• Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs
• Partial-order reduction in symbolic state-space exploration
• Proof-guided underapproximation-widening for multi-process systems
• Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
• Reduction
• An efficient partial order reduction algorithm with an alternative proviso implementation
• Title not available (Why is that?)
• Dynamic reductions for model checking concurrent software
• A calculus of atomic actions
• Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions

Cited In (11)

• Ant colony optimization with partial order reduction for discovering safety property violations in concurrent models
• Dynamic partial-order reduction for model checking software
• Space-reduction strategies for model checking dynamic 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
• Dynamic Path Reduction for Software Model Checking
• Title not available (Why is that?)

Uses Software

• VVT
• CTIGAR

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)