01
Clarke, Emerson, and Sifakis: Model Checking Becomes Automated Verification
Model checking combined temporal logic with exhaustive state-space algorithms, allowing finite-state hardware and software designs to be checked automatically and failures returned as counterexamples.
↗