A Recipe for Modular Verification of Generic Tree Traversals
summary
Presents a concrete verification recipe that models traversal state with a zipper with shadow and characterizes step types as action and silent steps, yielding a modular invariant that proves pre-, post- and in-order DFS traversals. Realizes the approach in RefinedC (Rocq) and verifies pointer- and array-based trees, variadic-arity trees, early termination, and traversals whose per-node operation can reshape whole subtrees. Proof effort splits into reusable logical, implementation, traversal, and client steps; artifacts and examples are available.
AI-written summary · about
chapters (15)
- 0:00Modular verification intro
- 1:24Higher-order traversals explained
- 3:49Modular verification recipe
- 5:55Mathematical abstraction of trees
- 7:20Invariant-based traversal specs
- 9:04Zipper-based state
- 11:07State progression formalized
- 12:53Action and silent steps
- 14:17Final traversal spec
- 15:40Evaluation with RefinedC
- 17:28Recap and contributions
- 18:09Q&A: List structures
- 18:53Q&A: Two-tree traversals
- 19:36Q&A: Full algorithm verification
- 20:39Q&A: Parent pointers
related talks
27mRooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separatio...
27mCompositional Verification of Concurrent C Programs with Search Structure Templat...
19mPredictable Verification using Intrinsic Definitions
17mModular Verification of Safe Memory Reclamation in Concurrent Separation Logic
15mGradual Verification of Recursive Heap Data Structures
15mModular Reasoning about Global Variables and Their Initialization
28mGradual Verification: Assuring Software Incrementally
15mModular Verification of Op-Based CRDTs in Separation Logic