An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures

DOI10.1007/978-3-540-69738-1_8MaRDI QIDQ5452601zbMATHOpenAlexFDO

Authors Zvonimir Rakamarić, Jesse Bingham, Alan J. Hu

Publication date 4 April 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-69738-1_8

Mathematics Subject Classification ID

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

Recommendations

• Verifying Heap-Manipulating Programs in an SMT Framework
• Verification, Model Checking, and Abstract Interpretation
• Modular reasoning about heap paths via effectively propositional formulas
• Forest automata for verification of heap manipulation
• Automated verification of recursive programs with pointers

Cites work

• scientific article; zbMATH DE number 1617328 (Why is no real title available?)
• scientific article; zbMATH DE number 1956566 (Why is no real title available?)
• scientific article; zbMATH DE number 1773084 (Why is no real title available?)
• scientific article; zbMATH DE number 2102703 (Why is no real title available?)
• An axiomatic basis for computer programming
• Automated Deduction – CADE-20
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• BI as an assertion language for mutable data structures
• Computer Aided Verification
• Computer Science Logic
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Foundations of Software Science and Computation Structures
• Grammar Analysis and Parsing by Abstract Interpretation
• Interprocedural Shape Analysis with Separated Heap Abstractions
• Lazy abstraction
• Predicate abstraction for software verification
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• 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

(5)

• Verification of heap manipulating programs with ordered data by extended forest automata
• Modular reasoning about heap paths via effectively propositional formulas
• Verification, Model Checking, and Abstract Interpretation
• Verifying Heap-Manipulating Programs in an SMT Framework
• Verification of heap manipulating programs with ordered data by extended forest automata

Describes a project that uses

Uses Software

• MONA

This page was built for publication: An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures

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