29. Check systems before they fail
Use temporal logic and state-space search to check whether a system can reach a bad state or must eventually do the right thing. This chapter follows the workflow behind model checking in software, hardware, and protocols.