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_8zbMATH Open1132.68354OpenAlexW1538691881MaRDI QIDQ5452601FDOQ5452601
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
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
Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- BI as an assertion language for mutable data structures
- Computer Science Logic
- An axiomatic basis for computer programming
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Grammar Analysis and Parsing by Abstract Interpretation
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Verification, Model Checking, and Abstract Interpretation
- Lazy abstraction
- Predicate abstraction for software verification
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Foundations of Software Science and Computation Structures
- Interprocedural Shape Analysis with Separated Heap Abstractions
- Verifying properties of well-founded linked lists
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
- Title not available (Why is that?)
- Title not available (Why is that?)
- Tools and Algorithms for the Construction and Analysis of Systems
- Automated Deduction – CADE-20
Cited In (4)
Uses Software
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)
