
Predicate abstraction for software verificationShaz Qadeer AbstractA completely automatic method for software verification is impossible since the problem is undecidable in general. Existing semiautomatic 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 generalpurpose 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.
Slides. 
Contact 
©20022018 U.C. Regents 