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_8zbMath1132.68354OpenAlexW1538691881MaRDI QIDQ5452601

Alan J. Hu, Zvonimir Rakamarić, Jesse Bingham

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

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

Related Items (1)

Verifying Heap-Manipulating Programs in an SMT Framework

Uses Software

• MONA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Grammar Analysis and Parsing by Abstract Interpretation
• Interprocedural Shape Analysis with Separated Heap Abstractions
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• BI as an assertion language for mutable data structures
• Lazy abstraction
• Predicate abstraction for software verification
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Science Logic
• Verifying properties of well-founded linked lists
• Automated Deduction – CADE-20
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• An axiomatic basis for computer programming
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation
• Foundations of Software Science and Computation Structures

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