A Recipe for Modular Verification of Generic Tree Traversals

Explore a novel approach to verifying generic tree traversal algorithms in this 22-minute conference presentation from CPP 2026. Learn how researchers from MPI-SWS, IST Austria, and Radboud University developed a comprehensive recipe for modular verification of stateful tree traversals that are commonly used in critical systems like page tables and web browser DOM implementations. Discover how their methodology addresses the challenges of verifying generic tree-traversal functions where client-provided operations can be stateful and may modify the tree structure during traversal. Examine the four key properties of their approach: generality across different traversal types (pre-order, post-order, and in-order depth-first), modularity for proof reuse, expressiveness for diverse client verification scenarios, and automation capabilities for discharging proof obligations. Understand the innovative use of tree zippers as logical abstractions for traversal state representation and zipper transitions for modeling traversal steps. See how the researchers implemented their recipe within the RefinedC framework in Rocq to successfully verify multiple tree traversals and their clients written in C, demonstrating practical applications in formal verification of low-level systems programming.