Predicate abstraction for software verification

Shaz Qadeer

Abstract

A completely automatic method for software verification is impossible since the problem is undecidable in general. Existing semi-automatic techniques that require annotations, such as loop invariants, from the programmer have had limited acceptance because the annotation burden on programmers is perceived to be excessive. In this talk, I will describe a method to infer loop invariants for programs written in a general-purpose programming language. We have implemented this method and used it to verify the exported procedure "create" from the implementation of a file system Frangipani.

Our method for inferring loop invariants has several nice features compared to previous methods. First, it can infer loop invariants with universal quantifications; this is critical in the verification of Frangipani whose specification comprises a number of assertions on unbounded data. Second, the method is based on forward analysis; it analyzes a loop in the context of the code preceding it resulting in more precision. At the core of our algorithm is predicate abstraction, a technique for characterizing a program in terms of how it transforms the truth values of a finite set of predicates. I will describe a novel algorithm for constructing the abstraction of a concrete set of states in terms of the predicates. I will also describe experimental results showing that our algorithm is more efficient in practice than existing algorithms.