A proof that does not finish is not a failure of the method; it is a model too large for the question. Abstraction replaces part of the model with something smaller. It is sound only under a stated condition, and each technique here has a run that passes where the condition holds and a run that fails or hides a fault where it does not. Cone-of-influence reduction is not on this menu: it is exact and automatic. An abstraction adds behaviour, and an assumption removes it.
Lesson | After it you can... |
|---|---|
Track one bit of a full-width model, and say which abstraction (narrowing) lies. | |
Shrink a threshold, find what the small size hides, and close the real size by induction. | |
Replace a memory by one tracked entry, constrain the address honestly and cover each region. | |
Cut a block free, read the false counterexample and write the minimal contract. |
Suggested order: top to bottom, from the cheapest abstraction (keep the structure, track less data) to the one that needs a proof of its own (cut a block and promise something about it).
What condition makes it sound for this design, and which run shows it can still fail: a fault that the abstract proof catches, and the condition broken on purpose.