Loop Verification with Invariants and Contracts

on YouTube ↗30m

" summary

Loop contracts pair an invariant with a relational summary and claim strictly more expressiveness than invariants alone while admitting a constructive translation to invariants so any verifier can implement them; examples include max by elimination, binary search and array copy where summaries simplify postconditions but can forget framing, so invariants still prevent runtime errors. Verification conditions are simple, tool experiments with Horn solvers are preliminary and inconclusive, and direct support is straightforward if the verifier allows spec-style pre/post statements.

AI-written summary · about

" chapters (11)

1. 0:00Start
2. 0:04Loop Verification with Invariants and Contracts
3. 3:07A Contract Consists of an Invariant
4. 3:49Finding the Maximum by Elimination
5. 6:02Recursive Algorithm
6. 10:52Proof for the Iterative Version
7. 14:23Summary Approach
8. 15:56What Is the Correspondence between Invariants and Summaries
9. 17:11Encode Summaries as Part of Invariant
10. 20:23Syntactic Proof Rule
11. 23:19Binary Search