Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separatio...
summary
Provides a library of definitions, lemmas and proof rules that let one switch between array and tree views (mutually derivable) to localize updates, formalizes non‑recursive traversals via a stack-top invariant that exactly characterizes stack and visited sets, and mechanises everything in Coq using Separation Logic and VST to verify a faithful C implementation of the tree‑clock join operation. The implementation verifies correctly, comes with artifacts, and shows measurable speedup over pointer‑based alternatives.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 0:23Array-based trees in separation logic
- 2:55Reasoning challenges
- 9:22Structure-changing operations
- 14:17Loop invariants for traversals
- 17:53Case study: Tree Clock
- 21:29Summary
- 22:19Q&A
related talks
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
22mA Recipe for Modular Verification of Generic Tree Traversals
21mEmbedding Hindsight Reasoning in Separation Logic
28mReasoning about Distributed Reconfigurable Systems
19mPete's Footprints
40mRelational Reasoning in Object-based Programs
57mInvited Talk: Bridging Safety and Performance
01h 09mPlenary: Neighborhoods Banding Together: Reasoning Globally about Programs