Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
DOI10.1007/s00165-019-00483-2zbMath1425.68285OpenAlexW2945420580WikidataQ127871360 ScholiaQ127871360MaRDI QIDQ2418047
A. W. Roscoe, Thomas Gibson-Robinson, Pedro Antonino
Publication date: 3 June 2019
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-019-00483-2
formal verificationmodel checkinglocal analysisSAT solvingdeadlock freedomapproximate verificationapproximate reachability
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Rigorous development of component-based systems using component metadata and patterns
- SAT-solving in CSP trace refinement
- The pursuit of deadlock freedom
- A stubborn attack on state explosion
- CCS expressions, finite state processes, and three problems of equivalence
- Symbolic model checking: \(10^{20}\) states and beyond
- Using integer programming to verify general safety and liveness properties
- Using partial orders for the efficient verification of deadlock freedom and safety properties
- Model checking of concurrent software systems via heuristic-guided SAT solving
- Understanding concurrent systems
- Tighter reachability criteria for deadlock-freedom analysis
- Concurrent software verification with states, events, and deadlocks
- Relationships between nondeterministic and deterministic tape complexities
- Deadlock analysis in networks of communicating processes
- A Static Analysis Framework for Livelock Freedom in CSP
- Analyzing Component-Based Systems on the Basis of Architectural Constraints
- The Automatic Detection of Token Structures and Invariants Using SAT Checking
- A Proof System for Communicating Sequential Processes
- Proving the Correctness of Multiprocess Programs
- Lazy Reachability Analysis in Distributed Systems
- Introduction to Distributed Algorithms
- Local Analysis of Determinism for CSP
- Checking Static Properties Using Conservative SAT Approximations for Reachability
- FDR3 — A Modern Refinement Checker for CSP
- Verification, Model Checking, and Abstract Interpretation
This page was built for publication: Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
