Plenary: Neighborhoods Banding Together: Reasoning Globally about Programs
summary
Local correctness proofs get collated into link-time tables and checked with an n log n graph algorithm: sort/unique build a forest, categorize edges as downward/upward/leftward, apply three rules (upward marks cycles, leftward propagates triangles left-to-right, downward participates only if its parallel path is cyclic) and reject cycles containing red marked edges while requiring at least one green marked decrement per cycle. Language extensions include interface adapters for pointers, virtuals, and member pointers and inline claimable recursion bounds; the process is concrete and decidable.
AI-written summary · about
chapters (12)
- 0:00Introduction to reasoning
- 0:35Local reasoning concepts
- 1:25Boundary conditions
- 3:36Game theory analogy
- 6:37Combining neighborhoods
- 10:04One Definition Rule
- 15:30Global reasoning techniques
- 20:58Interface adapters
- 30:05Solving recursion issues
- 35:59Graph theory for global check
- 44:05Recursion bounds in practice
- 50:29Conclusion and Q&A
related talks
59mKEYNOTE: The Shape of a Program
40mRelational Reasoning in Object-based Programs
28mReasoning about Distributed Reconfigurable Systems
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
19mPredictable Verification using Intrinsic Definitions
27mRooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separatio...
59mTheory makes beautiful programs