home

Books written by Edmund M. Clarke.

Together with E. Allen Emerson and Joseph Sifakis they won the Turing Award in 2007 for their roles in developing model checking into a highly effective verification technology, widely adopted in the hardware and software industries.

feynman

Model Checking

The main challenge in model checking is dealing with the state space explosion problem. This problem occurs in systems with many components that can interact with each other or systems with data structures that can assume many different values.
feynman

Handbook of Model Checking

Model checking is a computer-assisted method for the analysis of dynamical systems that can be modeled by state-transition systems. Drawing from research traditions in mathematical logic, programming languages, hardware design, and theoretical computer science, model checking is now widely used for the verification of hardware and software in industry.