Title: Program Analysis using Quantifier Elimination Heuristics

Presenter: Prof. Deepak Kapur  

Time: 10:00AM May 28, 2012 

Location: Room 230, CS Building, Xianlin Campus 

Abstract:        

    Loop invariants play a central role in ensuring the reliability of software. Program analysis techniques must either require such program annotations at appropriate program locations or automatically derive these annotations from a program. A new approach for automatically generating loop invariants from imperative programs will be presented. Loop Invariants are assumed to have certain shape, i.e., they are formulas in a restricted quantifier-free first-order theory. Elimination techniques can be used to generate such Invariants. The focus of this talk will be on exploring heuristics for quantifier-elimination, so that such techniques can scale well. A nice feature of the proposed approach is that it does not need to have access to any specification or annotations associated with a program. Some preliminary ideas about how to generalize these approaches to work on data types other than numbers will be discussed.