Quantified Heap Invariants for Object-Oriented Programs

DOI10.29007/zrctzbMath1403.68126OpenAlexW2741637561MaRDI QIDQ4645747

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

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

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 ⋮ Solving constrained Horn clauses over algebraic data types ⋮ Counterexample-guided prophecy for model checking modulo the theory of arrays ⋮ Reasoning in the theory of heap: satisfiability and interpolation

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