Taming Complexity
What to do when proofs do not converge: measure, reduce, cut, abstract, add helper invariants, decompose with assume-guarantee, split cases and choose engines — with worked examples.
What you will learn
- Diagnose why a proof is slow or inconclusive.
- Reduce the problem with parameters, black boxes and cut points while staying sound.
- Abstract counters and memories without losing the property.
- Use helper assertions, assume-guarantee decomposition and case splitting.
Lessons
- 10.1Diagnosing a hard proofMeasure before you optimise.
- 10.2Reducing the design: parameters, black boxes, cut pointsMake the model smaller — and know whether that is sound.
- 10.3Helper assertions and invariantsTeach the tool what you know about the design.
- 10.4Abstracting counters and memoriesReplace big state with small models that keep the property.
- 10.5Assume-guarantee and case splittingSplit one impossible proof into several possible ones.
- 10.6Engines, run strategy and bounded proofsGetting the most from the tool, and knowing when bounded is enough.
- ✎Chapter quiz (4 questions)