Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
Abstract elided by the publisher.
Related papers
- A Less Dynamic Memory Allocation Scheme for Algol-like Languages POPL 1984
- Modeling Dynamic (De)Allocations of Local Memory for Translation Validation OOPSLA 2024
- Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic CAV 2020
- Automatic formal verification of MPI-based parallel programs PPoPP 2011
- StarMalloc: Verifying a Modern, Hardened Memory Allocator OOPSLA 2024
- Deciding memory safety for single-pass heap-manipulating programs POPL 2020
- Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution) TACAS 2024
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic VMCAI 2017