Modular reasoning about heap paths via effectively propositional formulas
DOI10.1145/2535838.2535854zbMATH Open1284.68403OpenAlexW1976401986MaRDI QIDQ5408433FDOQ5408433
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
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
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)
Cited In (20)
- Verifying Heap-Manipulating Programs in an SMT Framework
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Propositional reasoning about safety and termination of heap-manipulating programs
- Verified heap theorem prover by paramodulation
- From invariant checking to invariant inference using randomized search
- Local reasoning for global graph properties
- Reachability modulo theories
- Verification, Model Checking, and Abstract Interpretation
- On Symbolic Heaps Modulo Permission Theories
- Model and proof generation for heap-manipulating programs
- Property Directed Reachability for Proving Absence of Concurrent Modification Errors
- Back to the future, revisiting precise program verification using SMT solvers
- Resourceful reachability as HORN-LA
- Decidable logics combining heap structures and data
- An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
- Satisfiability modulo heap-based programs
- A first-order logic with frames
- Structuring the verification of heap-manipulating programs
- What's decidable about program verification modulo axioms?
- Unified reasoning about robustness properties of symbolic-heap separation logic
Uses Software
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)
