Generalized Model Checking Patrice Godefroid   View Paper (PDF)   Return to Invited Talks Abstract Three-valued models, in which properties of a system are either true, false or unknown, have recently been advocated as a better representation for reactive program abstractions generated by automatic techniques such as predicate abstraction. Indeed, for the same cost, model checking three-valued abstractions (also called may/must abstractions) can be used to both prove and disprove any temporallogic property, whereas traditional conservative abstractions can only prove universal properties. Also, verification results can be more precise with generalized model checking, which checks whether there exists a concretization of an abstraction satisfying a temporal-logic formula. Generalized model checking generalizes both model checking (when the model is complete) and satisfiability (when everything in the model is unknown), probably the two most studied problems related to temporal logic and verification. In this talk, I will present the main ideas behind this framework, namely models for three-valued abstractions, completeness preorders (to measure the level of completeness of such models), three-valued temporal logics and generalized model checking. I will also discuss algorithms and complexity bounds for three-valued model checking and generalized model-checking for various temporal logics. Then, I will discuss applications to program verification via automatic abstraction. I will show examples of programs and properties that can be verified by generalized model checking but not with current abstraction-based verification tools. I will also present classes of temporal-logic formulas for which model checking is guaranteed to always have the same precision as generalized model checking. Finaly, I will briefly discuss three-valued abstractions for reasoning about open systems and about games in general, as well as completeness issues (i.e., given an infinite-state program and a property, is there a finite-state abstraction of that program that satisfies this property?). ©2006 Association for Computing Machinery