Madhavan Mukund

Model-checking: Automated Verification of Computational Systems

Madhavan Mukund

Resonance, July 2009


The ACM Turing Award for 2007 was awarded to Clarke, Emerson and Sifakis for their invention of model-checking, an automated technique for verifying finite-state computing systems. In this article, we describe the central ideas underlying their approach.

  • Download PDF.