Property Directed Reachability for Proving Absence of Concurrent Modification Errors

DOI10.1007/978-3-319-52234-0_12MaRDI QIDQ2961566zbMATH OpenOpenAlexFDO

Authors Asya Frumkin, Yotam M. Y. Feldman, Ondřej Lhoták, Oded Padon, Mooly Sagiv, 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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Property preserving abstractions for the verification of concurrent systems
• Reachability in Concurrent Uninterpreted Programs.
• The Lattice-Theoretic Essence of Property Directed Reachability Analysis
• Generalized property directed reachability
• Adequate proof principles for invariance and liveness properties of concurrent programs
• Formal verification of concurrent systems via directed model checking

Cites work

• Deciding effectively propositional logic using DPLL and substitution sets
• Generalized property directed reachability
• Modular reasoning about heap paths via effectively propositional formulas
• Property-directed inference of universal invariants or proving their absence
• SAT-Based Model Checking without Unrolling
• SMT-based model checking for recursive programs
• Verification, Model Checking, and Abstract Interpretation

Cited in

(3)

• Property-directed inference of universal invariants or proving their absence
• Property-directed inference of universal invariants or proving their absence
• Verifying safety properties of concurrent Java programs using 3-valued logic

Describes a project that uses

Uses Software

• Spacer
• Soot
• Ivy
• MONA
• z3

This page was built for publication: Property Directed Reachability for Proving Absence of Concurrent Modification Errors

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