Dynamic partial-order reduction for model checking software

DOI10.1145/1040305.1040315zbMATH Open1369.68135OpenAlexW2169870841MaRDI QIDQ5276139FDOQ5276139

Authors: 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

Recommendations

• scientific article; zbMATH DE number 2087625
• Dynamic reductions for model checking concurrent software
• Formal verification of a partial-order reduction technique for model checking
• Partial-order reduction techniques for real-time model checking
• Dynamic Path Reduction for Software Model Checking
• Combining partial-order reductions with on-the-fly model-checking.
• scientific article; zbMATH DE number 1361136

zbMATH Keywords

software model checkingpartial-order reduction

Mathematics Subject Classification ID

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

Cited In (58)

• Compositional verification of priority systems using sharp bisimulation
• Unfolding-based dynamic partial order reduction of asynchronous distributed programs
• What's wrong with on-the-fly partial order reduction
• Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods
• Reconciling preemption bounding with DPOR
• Unblocking dynamic partial order reduction
• A geometric view of partial order reduction
• Model checking concurrent programs
• Partial order reduction for deep bug finding in synchronous hardware
• Stateless model checking under a reads-value-from equivalence
• Goal-driven unfolding of Petri nets
• Title not available (Why is that?)
• Exploring the scope for partial order reduction
• Analysis and Transformation of Constrained Horn Clauses for Program Verification
• Actor-based model checking for software-defined networks
• SDN-actors: modeling and verification of SDN programs
• Hybrid analysis for partial order reduction of programs with arrays
• Software model checking with explicit scheduler and symbolic threads
• Title not available (Why is that?)
• Symmetry and partial order reduction techniques in model checking Rebeca
• Composing model programs for analysis
• Quantifiability: a concurrent correctness condition modeled in vector space
• Stateless model checking for TSO and PSO
• Dynamic reductions for model checking concurrent software
• Symbolic predictive analysis for concurrent programs
• Peephole Partial Order Reduction
• Prefix-based tracing in message-passing concurrency
• Approximate partial order reduction
• Local Data Race Freedom with Non-multi-copy Atomicity
• Context-aware counter abstraction
• A pragmatic approach to stateful partial order reduction
• Operational semantics with semicommutations
• Combining model checking and testing
• Global reproducibility through local control for distributed active objects
• Optimising the ProB model checker for B using partial order reduction
• Combining partial-order reductions with on-the-fly model-checking.
• Multithreaded testing of program interfaces
• Partial order reduction for rewriting semantics of programming languages
• Dynamic Partial Order Reduction Using Probe Sets
• Computing race variants in message-passing concurrent programming with selective receives
• POR for security protocol equivalences. Beyond action-determinism
• Quasi-optimal partial order reduction
• Model Checking Software
• Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings
• Compositional verification of asynchronous concurrent systems using CADP
• Automatic analysis of DMA races using model checking and \(k\)-induction
• Bisimulation conversion and verification procedure for goal-based control systems
• Full simulation coverage for SystemC transaction-level models of systems-on-a-chip
• A Study of Model-Order Reduction Techniques for Verification
• Sound and complete monitoring of sequential consistency for relaxed memory models
• Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs
• Efficient trace encodings of bounded synthesis for asynchronous distributed systems
• Verification of SpecC using predicate abstraction
• Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions
• Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
• Dynamic Path Reduction for Software Model Checking
• Independence abstractions and models of concurrency
• Verifying the correctness of distributed systems via mergeable parallelism

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5276139)