Combining model checking and deduction

Abstract

There are two basic approaches to automated verification. In model checking, the system is viewed as a graph representing possible execution steps. Properties are established by exploring or traversing the graph structure. In deduction, both the system and its putative properties are represented by formulas in a logic, and the resulting proof obligations are discharged by decision procedures or by automated or semi-automated proof construction. Model checking sacrifices expressivity for greater automation, and with deduction it is vice versa. Newer techniques combine deductive and model-checking approaches to achieve greater scale, expressivity, and automation. We examine the logical foundations of the two approaches and explore their similarities, differences, and complementarities. The presentation is directed at students and researchers who are interested in understanding the research challenges at the intersection of deduction and model checking.