Model Checking

Model Checking is a technique to prove a concurrent system finite model satisfies a given property. Largely used to prove hardware systems correct, new techniques allow its use also to verify software systems. This paper aims to present a tutorial overview of the fundamental principles of model checking, as presented in the WEIT 2011. The mais goal is to motivate undergraduate students to pursuit knowledge is this exciting area and to seek for the large body of available model checking literature and tools.