K-induction asks you to write the invariant. Two families of engines write it themselves: clause learners that grow frames of reachable states until one is inductive, and interpolation engines that over-approximate the states reachable within a bound. Both are taught here at concept level on paper-sized systems, because the ideas, not the solver internals, are what you need to read their verdicts and their evidence.
Lesson | After it you can... |
|---|---|
Explain frames, blocking and propagation, and what a grown invariant means. | |
State the two interpolant conditions and when the loop has to lengthen its bound. | |
Review an engine-found invariant and compare it with a hand-written helper. |
Suggested order: top to bottom. Frames first, because interpolation reuses the over-approximation idea. Interpolation second, because it relates back to the bound you already know. Reading engine output last, because it applies both to the working FIFO proof you can run.
The invariant itself: k-induction checks a helper you wrote, while a learning engine grows one from the design and the property. Both end at an inductive invariant; they differ in who writes it.