Using partial orders for the efficient verification of deadlock freedom and safety properties

DOI10.1007/BF01383879zbMath0772.68064MaRDI QIDQ1801499

Pierre Wolper, Patrice Godefroid

Publication date: 17 August 1993

Published in: Formal Methods in System Design (Search for Journal in Brave)

zbMATH Keywords

concurrent programmingstate-space explosiondeadlock detectionstate-space exploration

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (35)

Stubborn set reduction for timed reachability and safety games ⋮ Automated Synthesis of Distributed Controllers ⋮ Using integer programming to verify general safety and liveness properties ⋮ Partial-Order Reduction ⋮ Interpreting message flow graphs ⋮ Question-guided stubborn set methods for state properties ⋮ On Distributed Monitoring and Synthesis ⋮ An application of temporal projection to interleaving concurrency ⋮ Unnamed Item ⋮ Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving ⋮ Partial-order reduction in the weak modal mu-calculus ⋮ A pragmatic approach to stateful partial order reduction ⋮ Untanglings: a novel approach to analyzing concurrent systems ⋮ Deadlock-freedom in component systems with architectural constraints ⋮ Dynamic Partial Order Reduction Using Probe Sets ⋮ Reduced state space representation for unbounded vector state spaces ⋮ Reachability analysis based on structured representations ⋮ Covering step graph ⋮ A stubborn attack on state explosion ⋮ Automatic verification of distributed systems: the process algebra approach. ⋮ Compositional CSP Traces Refinement Checking ⋮ Ensuring completeness of symbolic verification methods for infinite-state systems ⋮ On commutativity based edge lean search ⋮ Handling Parameterized Systems with Non-atomic Global Conditions ⋮ Hierarchical Adaptive State Space Caching Based on Level Sampling ⋮ Optimising the ProB model checker for B using partial order reduction ⋮ Using partial orders for the efficient verification of deadlock freedom and safety properties ⋮ Compositional minimisation of finite state systems using interface specifications ⋮ MONOTONIC ABSTRACTION: ON EFFICIENT VERIFICATION OF PARAMETERIZED SYSTEMS ⋮ Analyzing a \(\chi\) model of a turntable system using Spin, CADP and Uppaal ⋮ Using heuristic search for finding deadlocks in concurrent systems ⋮ Model checking of systems with many identical timed processes ⋮ Automated Synthesis: a Distributed Viewpoint ⋮ Automated formal analysis and verification: an overview ⋮ Compositional verification of asynchronous concurrent systems using CADP

Uses Software

• CESAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Adequate proof principles for invariance and liveness properties of concurrent programs
• The complementation problem for Büchi automata with applications to temporal logic
• Recognizing safety and liveness
• A partial approach to model checking
• Using partial orders for the efficient verification of deadlock freedom and safety properties
• Exponential Determinization for ω‐Automata with a Strong Fairness Acceptance Condition
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Proving Liveness Properties of Concurrent Programs
• Decidability of Second-Order Theories and Automata on Infinite Trees

This page was built for publication: Using partial orders for the efficient verification of deadlock freedom and safety properties