Automatic Termination Proofs for Programs with Shape-Shifting Heaps
From MaRDI portal
Recommendations
Cited in
(22)- Heaps and Data Structures: A Challenge for Automated Provers
- Inference of field-sensitive reachability and cyclicity
- Decision Procedures for Automating Termination Proofs
- Automatic numeric abstractions for heap-manipulating programs
- Automata-Based Termination Proofs
- Proving termination and memory safety for programs with pointer arithmetic
- Verification of multi-linked heaps
- Programs with lists are counter automata
- Termination graphs for Java bytecode
- Proof Pearl: The Termination Analysis of Terminator
- Tools and Algorithms for the Construction and Analysis of Systems
- scientific article; zbMATH DE number 7453196 (Why is no real title available?)
- Cyclic proofs of program termination in separation logic
- Automatically proving termination and memory safety for programs with pointer arithmetic
- From shape analysis to termination analysis in linear time
- Monotonic Abstraction for Programs with Dynamic Memory Heaps
- Proving Termination of Tree Manipulating Programs
- Proving Termination of C Programs with Lists
- Separation Logic Tutorial
- Heap Assumptions on Demand
- Automata-based termination proofs
- Local reasoning about data update
This page was built for publication: Automatic Termination Proofs for Programs with Shape-Shifting Heaps
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5756731)
