Tutorial

Ken McMillan - Invariant Generation

Abstract: Invariant generation is at the heart of both model checking and deductive approaches to verification. In this tutorial, we'll survey the existing approaches to automated invariant generation methods, looking for commonalities and differences in the ways the techniques deal with the fundamental tensions in invariant generation, and especially for ways in which the different approaches might reinforce each other. We'll consider fixed-point methods (such as abstract interpretation, symbolic model checking and invisible invariants), interpolant-based methods, and template-based methods.