Property Directed Reachability for Proving Absence of Concurrent Modification Errors
From MaRDI portal
Publication:2961566
DOI10.1007/978-3-319-52234-0_12zbMath1484.68047OpenAlexW2571471892MaRDI QIDQ2961566
Asya Frumkin, Mooly Sagiv, Yotam M. Y. Feldman, Ondřej Lhoták, Oded Padon, Sharon Shoham
Publication date: 21 February 2017
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-52234-0_12
Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Uses Software
Cites Work
- SMT-based model checking for recursive programs
- Deciding effectively propositional logic using DPLL and substitution sets
- Property-directed inference of universal invariants or proving their absence
- Generalized Property Directed Reachability
- SAT-Based Model Checking without Unrolling
- Modular reasoning about heap paths via effectively propositional formulas
- Verification, Model Checking, and Abstract Interpretation