Tata Institute of Fundamental Research
Program Analysis Using Quantifier Elimination Heuristics
Seminar
Speaker:
Deepak Kapur (The University of New Mexico
Department of Computer Science
Albuquerque, NM 87131
United States of America)
Organiser:
Paritosh K Pandya
Date:
Tuesday, 8 Jan 2013, 11:00 to 12:00
Venue:
AG-80
(Scan to add to calendar)
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.
| Speaker: | Deepak Kapur (The University of New Mexico Department of Computer Science Albuquerque, NM 87131 United States of America) |
| Organiser: | Paritosh K Pandya |
| Date: | Tuesday, 8 Jan 2013, 11:00 to 12:00 |
| Venue: | AG-80 |
(Scan to add to calendar)
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.