Predicate abstraction for software verification

e Abstraction for Software Verification Cormac Flanagan Shaz Qadeer Compaq Systems Research Center 130 Lytton Ave, Palo Alto, CA 94301 Software verification is an important and difficult problem. Many static checking techniques for software require annotations from the programmer in the form of method specifications and loop invariants. This annotation overhead, particularly of loop invariants, is a significant hurdle in the acceptance of static checking. We reduce the annotation burden by inferring loop invariants automatically. od is based on predicate abstraction, an interpretation technique in which the abstract domain is constructed from a given set of predicates over program variables. A novel feature of our approach is that it infers universally-quantified loop invariants, which are crucial for verifying programs that manipulate unbounded data such as arrays. We present heuristics for generating appropriate predicates for each loop automatically; the programmer can specify addi...

• Type: Conference
• Year: 2002
• Where: POPL
• Authors: Cormac Flanagan, Shaz Qadeer
• Keywords: Cormac Flanagan Shaz, Loop Invariants, POPL 2002, Programming Languages, Qadeer Compaq Systems