Dynamic Reductions for Model Checking Concurrent Software

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

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

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

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

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Dynamic partial-order reduction for model checking software
• SAT-Based Model Checking without Unrolling
• 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
• 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 (3)

• Ant colony optimization with partial order reduction for discovering safety property violations in concurrent models
• Dynamic partial-order reduction for model checking software
• Dynamic Reductions for Model Checking Concurrent Software

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)