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

Horn clause solvingmemory modelssoftware model checking

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60)

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)

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