Every verdict a formal tool reports is a statement about reachable states: either no bad state is reachable, here is a path to one, or the search gave up. This topic builds that picture from the ground up on the decade counter, shows how engines store and search state symbolically instead of one state at a time, and lays out the engine menu so that every later topic can name the engine it is driving.
Lesson | After it you can... |
|---|---|
Compute a reachable set by hand and say why a safety property is a reachability question. | |
Explain how state sets are stored and how one step becomes solver clauses. | |
Pick the engine that fits the design and predict what dominates its cost. | |
Read two disagreeing runs and name the model, assumption, reset or limit that differs. |
Suggested order: top to bottom. Reachability first, because every engine verdict is a reachability claim. Storage and search second, because cost arguments later refer to them. The engine menu third, because choosing an engine needs the first two. The disagreeing-runs lesson last, because it applies the whole topic to the most argued-about situation in reviews.
Because every engine answers the same question, whether a bad state is reachable, and differs only in how it stores and searches the set. The vocabulary of states, steps and reachability is shared; the engines are interchangeable tools over it.