Dynamic partial-order reduction for model checking software

DOI10.1145/1040305.1040315zbMath1369.68135OpenAlexW2169870841MaRDI QIDQ5276139

Cormac Flanagan, Patrice Godefroid

Publication date: 14 July 2017

Published in: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://escholarship.org/uc/item/47c9f29c

zbMATH Keywords

software model checkingpartial-order reduction

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (40)

A geometric view of partial order reduction ⋮ Local Data Race Freedom with Non-multi-copy Atomicity ⋮ Global Reproducibility Through Local Control for Distributed Active Objects ⋮ Stateless model checking under a reads-value-from equivalence ⋮ Verification of SpecC using predicate abstraction ⋮ Model Checking Concurrent Programs ⋮ Combining Model Checking and Testing ⋮ Symmetry and partial order reduction techniques in model checking Rebeca ⋮ Verifying the correctness of distributed systems via mergeable parallelism ⋮ Computing race variants in message-passing concurrent programming with selective receives ⋮ Multithreaded testing of program interfaces ⋮ POR for security protocol equivalences. Beyond action-determinism ⋮ Context-aware counter abstraction ⋮ Stateless model checking for TSO and PSO ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Prefix-based tracing in message-passing concurrency ⋮ A pragmatic approach to stateful partial order reduction ⋮ Quantifiability: a concurrent correctness condition modeled in vector space ⋮ Independence Abstractions and Models of Concurrency ⋮ Dynamic Reductions for Model Checking Concurrent Software ⋮ Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings ⋮ Unfolding-based dynamic partial order reduction of asynchronous distributed programs ⋮ Bisimulation conversion and verification procedure for goal-based control systems ⋮ Symbolic predictive analysis for concurrent programs ⋮ Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions ⋮ Dynamic Partial Order Reduction Using Probe Sets ⋮ Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems ⋮ Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models ⋮ Actor-based model checking for software-defined networks ⋮ Composing model programs for analysis ⋮ SDN-actors: modeling and verification of SDN programs ⋮ Approximate partial order reduction ⋮ Operational semantics with semicommutations ⋮ Unnamed Item ⋮ Quasi-optimal partial order reduction ⋮ Automatic analysis of DMA races using model checking and \(k\)-induction ⋮ Exploring the Scope for Partial Order Reduction ⋮ Full simulation coverage for SystemC transaction-level models of systems-on-a-chip ⋮ Compositional verification of asynchronous concurrent systems using CADP ⋮ Partial Order Reduction for Rewriting Semantics of Programming Languages

This page was built for publication: Dynamic partial-order reduction for model checking software