Automatic Termination Proofs for Programs with Shape-Shifting Heaps

DOI10.1007/11817963_35zbMath1188.68109OpenAlexW2136242294MaRDI QIDQ5756731

Dino Distefano, Josh Berdine, Byron Cook, Peter W. O'Hearn

Publication date: 5 September 2007

Published in: Computer Aided Verification (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11817963_35

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (11)

Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Inference of Field-Sensitive Reachability and Cyclicity ⋮ Monotonic Abstraction for Programs with Dynamic Memory Heaps ⋮ Verification of multi-linked heaps ⋮ Unnamed Item ⋮ Programs with lists are counter automata ⋮ Termination Graphs for Java Bytecode ⋮ Decision Procedures for Automating Termination Proofs ⋮ Automata-Based Termination Proofs ⋮ Separation Logic Tutorial ⋮ Local Reasoning about Data Update

This page was built for publication: Automatic Termination Proofs for Programs with Shape-Shifting Heaps