model checking
How do you become certain that a chip design or a concurrency protocol has no fatal bug — not just that it passed the tests you happened to think of, but that a bad thing can never happen on any possible execution? Testing samples a few runs; model checking does something far stronger. It exhaustively and automatically explores every reachable state of a system to prove that a desired property holds in all of them, or to produce a concrete counterexample showing exactly how it fails.
The recipe has three ingredients. First, you build a model of the system as a finite (or finitely described) state machine: states are configurations, transitions are the possible steps. Second, you write the property you want as a temporal-logic formula (for example 'the system never deadlocks' or 'every request is eventually served'). Third, the model checker mechanically decides whether every behaviour of the model satisfies the formula. The automata connection makes this concrete: the temporal formula becomes a Buchi automaton, and checking reduces to asking whether the product of the system and the negated property has any accepting infinite run — if it does, that run is a bug trace; if not, the property is proved. The famous obstacle is state explosion: the number of states grows exponentially with the number of components, which symbolic methods (representing huge state sets compactly) and clever abstractions fight to tame.
Model checking is one of the great real-world payoffs of automata theory and logic. It is routine in hardware design (verifying processors and cache-coherence protocols), and used for device drivers, communication and security protocols, and safety-critical control software. Its power and its limit are the same fact: it gives a genuine proof over the model you built, so a verified model with a wrong or incomplete model of reality can still mislead you — model checking verifies the model, and is only as trustworthy as that model and the property you wrote.
To verify a traffic-light controller never shows green to both directions at once, you model its states and transitions, write the safety property G not(greenNS and greenEW), and run a model checker. It explores every reachable state; if no state has both greens it reports the property holds, and if some sequence of events reaches a double-green it hands back that exact sequence as a counterexample to fix.
Model checking exhaustively explores all states to prove a property or return a concrete bug trace.
Model checking verifies the MODEL you built against the property you wrote — it proves something genuine, but a faithful-looking model that misrepresents reality, or a mis-stated property, can yield a 'verified' system that still fails. State explosion is the central practical challenge.