Modular reasoning about heap paths via effectively propositional formulas

DOI10.1145/2535838.2535854MaRDI QIDQ5408433zbMATH OpenOpenAlexFDO

Authors Shachar Itzhaky, Anindya Banerjee, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv, Neil Immerman

Publication date 10 April 2014

Published in Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2535838.2535854

zbMATH Keywords

linked listsmtverification

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Satisfiability modulo heap-based programs
• Verification, Model Checking, and Abstract Interpretation
• Verifying Heap-Manipulating Programs in an SMT Framework
• An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
• Program Verification with Separation Logic

Cited in

(20)

• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• Propositional reasoning about safety and termination of heap-manipulating programs
• Resourceful reachability as HORN-LA
• Property Directed Reachability for Proving Absence of Concurrent Modification Errors
• Unified reasoning about robustness properties of symbolic-heap separation logic
• Back to the future, revisiting precise program verification using SMT solvers
• Verifying Heap-Manipulating Programs in an SMT Framework
• Satisfiability modulo heap-based programs
• Local reasoning for global graph properties
• A first-order logic with frames
• On Symbolic Heaps Modulo Permission Theories
• What's decidable about program verification modulo axioms?
• Reachability modulo theories
• Verified heap theorem prover by paramodulation
• From invariant checking to invariant inference using randomized search
• Structuring the verification of heap-manipulating programs
• Decidable logics combining heap structures and data
• Model and proof generation for heap-manipulating programs
• An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
• Verification, Model Checking, and Abstract Interpretation

Describes a project that uses

Uses Software

• Spec#
• z3
• SMT-LIB

This page was built for publication: Modular reasoning about heap paths via effectively propositional formulas

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