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

verificationlinked listsmt

Mathematics Subject Classification ID

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)

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)

• What's decidable about program verification modulo axioms?
• Unified reasoning about robustness properties of symbolic-heap separation logic
• 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
• From invariant checking to invariant inference using randomized search
• Verified heap theorem prover by paramodulation
• Local reasoning for global graph properties
• Reachability modulo theories
• On Symbolic Heaps Modulo Permission Theories
• Verification, Model Checking, and Abstract Interpretation
• Model and proof generation for heap-manipulating programs
• Property Directed Reachability for Proving Absence of Concurrent Modification Errors
• Resourceful reachability as HORN-LA
• Back to the future, revisiting precise program verification using SMT solvers
• 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

Describes a project that uses

Uses Software

• z3
• Spec#
• 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)