Cyclic Abduction of Inductively Defined Safety and Termination Preconditions
No abstract available.
Related papers
- Maximal Quantified Precondition Synthesis for Linear Array Loops ESOP 2024
- Cyclic proofs of program termination in separation logic POPL 2008
- Automatic cyclic termination proofs for recursive procedures in separation logic CPP 2017
- Weakest Precondition Inference for Non-Deterministic Linear Array Programs TACAS 2024
- An abstract interpretation framework for termination POPL 2012
- Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs ESOP 2015
- HipTNT+: A Termination and Non-termination Analyzer by Second-Order Abduction - (Competition Contribution) TACAS 2017
- Omnisemantics: Smooth Handling of Nondeterminism TOPLAS 2023