Automatic Termination Proofs for Programs with Shape-Shifting Heaps
From MaRDI portal
Publication:5756731
DOI10.1007/11817963_35zbMath1188.68109MaRDI 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
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Unnamed Item, Separation Logic Tutorial, Verification of multi-linked heaps, Programs with lists are counter automata, Automatically proving termination and memory safety for programs with pointer arithmetic, Local Reasoning about Data Update, Inference of Field-Sensitive Reachability and Cyclicity, Termination Graphs for Java Bytecode, Decision Procedures for Automating Termination Proofs, Monotonic Abstraction for Programs with Dynamic Memory Heaps, Automata-Based Termination Proofs