Quantified Heap Invariants for Object-Oriented Programs

DOI10.29007/ZRCTMaRDI QIDQ4645747zbMATH OpenOpenAlexFDO

Authors Temesghen Kahsai, Rody Kersten, Philipp Rümmer, Martin Schäf

Publication date 10 January 2019

Published in EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.29007/zrct

zbMATH Keywords

memory modelssoftware model checkingHorn clause solving

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) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• A generic framework for heap and value analyses of object-oriented programming languages
• Statically inferring complex heap, array, and numeric invariants
• Structuring the verification of heap-manipulating programs
• Logical Approaches to Computational Barriers
• An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software

Cited in

(17)

• scientific article; zbMATH DE number 1953023 (Why is no real title available?)
• Reversible Representation and Manipulation of Constructor Terms in the Heap
• RustHorn: CHC-based verification for Rust programs
• On the adequacy of dependence-based representations for programs with heaps
• Reasoning in the theory of heap: satisfiability and interpolation
• A generic framework for heap and value analyses of object-oriented programming languages
• Counterexample-guided prophecy for model checking modulo the theory of arrays
• Counterexample-guided focus
• Solving constrained Horn clauses over algebraic data types
• A program instrumentation framework for automatic verification
• ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
• Efficient bounded model checking of heap-manipulating programs using tight field bounds
• Statically inferring complex heap, array, and numeric invariants
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
• Monotonic Abstraction for Programs with Dynamic Memory Heaps
• scientific article; zbMATH DE number 1956604 (Why is no real title available?)
• Automatic program instrumentation for automatic verification

This page was built for publication: Quantified Heap Invariants for Object-Oriented Programs

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