Verifying Heap-Manipulating Programs in an SMT Framework
From MaRDI portal
Publication:3510799
DOI10.1007/978-3-540-75596-8_18zbMath1141.68484OpenAlexW1519981183WikidataQ62041333 ScholiaQ62041333MaRDI QIDQ3510799
Alessandro Cimatti, Alan J. Hu, Zvonimir Rakamarić, Roberto Bruttomesso
Publication date: 3 July 2008
Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-75596-8_18
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
Verification of heap manipulating programs with ordered data by extended forest automata ⋮ Separation logics and modalities: a survey ⋮ Invariants Synthesis over a Combined Domain for Automated Program Verification
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Predicate abstraction of ANSI-C programs using SAT
- Efficient theory combination via Boolean search
- Solvable cases of the decision problem
- Simplify: a theorem prover for program checking
- Simplification by Cooperating Decision Procedures
- Lazy abstraction
- Computer Science Logic
- Verifying properties of well-founded linked lists
- Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
- Automated Deduction – CADE-20
- Structural Abstraction of Software Verification Conditions
- Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
- 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
- Verification, Model Checking, and Abstract Interpretation
- Computer Aided Verification
- Computer Aided Verification
- A Reachability Predicate for Analyzing Low-Level Software
- Combined Satisfiability Modulo Parametric Theories
- Verification, Model Checking, and Abstract Interpretation
- Foundations of Software Science and Computation Structures
- Formal Methods at the Crossroads. From Panacea to Foundational Support
This page was built for publication: Verifying Heap-Manipulating Programs in an SMT Framework
