Generalized Arrays for Stainless Frames
summary
Implements a verification pipeline in Stainless (Scala) that encodes dynamic frames without quantifiers by lowering heaps to arrays and emitting Z3’s extended array theory, claiming quantifier-free frame encoding that preserves decidability and yields concrete counterexamples. Uses a new map merge combinator and heap-unchanged primitives to project read/modify footprints, exposes first-class ghost heap values and history snapshots, and verifies examples: stacks, mutable and cyclic linked lists, and a function cache. Tool integration with Inox/Z3 produces proofs and concrete counterexamples.
AI-written summary · about
chapters (19)
- 0:00Introduction
- 2:40Overview
- 5:20Example
- 6:20Stack
- 7:40Wrapper
- 8:45Stack Data Structure
- 10:25Heap Encoding
- 12:00Frame Conditions
- 13:35Frame axioms
- 14:15Approach
- 15:05Relogic
- 16:35Map combinator
- 17:40Map merge
- 19:45Heap unchanged
- 21:05Encoding missing frames
- 23:00Flexibility
- 25:30Stainless benchmarks
- 26:15Conclusion
- 27:00QA
related talks
22mImplementing separation logic using an SMT-backed Frame Rule
16mIndexed Streams: A Formal Intermediate Representation for Fused Contraction Programs
19mPanel: Compilation Frameworks
51mArrays 2.0 - Opportunities and Challenges
23mApple Array Allocation
11mExtending the Scope of the Array Abstraction beyond Sparsity
01h 05mAll the Languages Together
26mMechanical Proofs in an Array-Combinator Language