Verifying Heap-Manipulating Programs in an SMT Framework

DOI10.1007/978-3-540-75596-8_18MaRDI QIDQ3510799zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Zvonimir Rakamarić, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Back to the future, revisiting precise program verification using SMT solvers
• An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
• Modular reasoning about heap paths via effectively propositional formulas
• Satisfiability modulo heap-based programs
• Verification, Model Checking, and Abstract Interpretation

Cites work

• A Reachability Predicate for Analyzing Low-Level Software
• An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
• Automated Deduction – CADE-20
• Combined Satisfiability Modulo Parametric Theories
• Combining decision procedures.
• Computer Aided Verification
• Computer Aided Verification
• Computer Science Logic
• Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
• Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
• Efficient theory combination via Boolean search
• Foundations of Software Science and Computation Structures
• scientific article; zbMATH DE number 1617328 (Why is no real title available?)
• scientific article; zbMATH DE number 1773084 (Why is no real title available?)
• Lazy abstraction
• Predicate abstraction of ANSI-C programs using SAT
• Simplification by Cooperating Decision Procedures
• Simplify: a theorem prover for program checking
• Solvable cases of the decision problem
• Structural Abstraction of Software Verification Conditions
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Verifying properties of well-founded linked lists

Cited in

(9)

• Invariants synthesis over a combined domain for automated program verification
• Verification of heap manipulating programs with ordered data by extended forest automata
• Back to the future, revisiting precise program verification using SMT solvers
• Separation logics and modalities: a survey
• Modular reasoning about heap paths via effectively propositional formulas
• 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
• SMT-based verification of program changes through summary repair
• The decision problem for undirected graphs with reachability and acyclicity

Describes a project that uses

Uses Software

• Spec#
• SIMPLIFY
• TVLA
• ESC/Java

This page was built for publication: Verifying Heap-Manipulating Programs in an SMT Framework

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