Model and Proof Generation for Heap-Manipulating Programs
No abstract available.
Related papers
- Certifying the synthesis of heap-manipulating programs ICFP 2021
- Structuring the synthesis of heap-manipulating programs POPL 2019
- Natural proofs for data structure manipulation in C using separation logic PLDI 2014
- Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs ESOP 2015
- Effective Entailment Checking for Separation Logic with Inductive Definitions TACAS 2019
- Certifying graph-manipulating C programs via localizations within data structures OOPSLA 2019
- Sound and Complete Invariant-Based Heap Encodings OOPSLA 2026
- Automated lemma synthesis in symbolic-heap separation logic POPL 2018