Model checking

Model checking is increasingly being perceived as the prime industrially relevant approach to (formal) system verification. This is due partly to the high level of automation it allows and partly to the ease with which it can be inserted in existing design-flows. Its natural application domain is systems that are primarily control (as opposed to data) driven and that have a high level of interaction with an only partly controllable environment. Indeed, model checking has seen most use in telecommunication and in hardware design. Moreover, companies such as Siemens and Intel have incorporated these methods into their system design-flows. Conceptually, model checking explores the space of all possible system behaviors in search for an illegal one that refutes some system requirement. Indeed, in some implementations this exploration resembles an SLD refutation with a depth-first search rule. Accordingly, a major issue is the efficiency of such searches, which entails questions of compact representation of behaviors, early pruning of the search space (e.g., automatic insertion of safe cuts) and the use of abstract interpretation. A second example is in the application of model checking to systems that have a continously varying component. Behaviors of such systems cannot be enumerated anymore and one uses a constraint system instead to describe the behavior space and searches for a refuting behavior in the solution set. This tutorial aims to give an introduction and overview of model checking; its methods, its applications, its limits. Secondly, it aims to indicate those spots where model checking and logic programming touch and where awareness of results and research directions can be mutually beneficial.