Array Abstractions from Proofs
Abstract elided by the publisher.
Related papers
- Bridging Arrays and ADTs in Recursive Proofs TACAS 2021
- Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic CPP 2024
- 2LS: Arrays and Loop Unwinding - (Competition Contribution) TACAS 2023
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays TACAS 2021
- Regular Abstractions for Array Systems POPL 2024
- Verifying Array Properties in Pure Data-Parallel Programs PLDI 2026
- Mechanised Hypersafety Proofs about Structured Data PLDI 2024
- Non-disjunctive Numerical Domain for Array Predicate Abstraction ESOP 2008