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.