Tata Institute of Fundamental Research
When is a Formula Invariant?
Seminar
Speaker:
Deepak Kapur (University of New Mexico
Department of Computer Science
School of Engineering
Albuquerque, NM 87131-0001
United States of America)
Organiser:
Paritosh K Pandya
Date:
Friday, 21 Feb 2014, 16:00 to 17:30
Venue:
D-405 (D-Block Seminar Room)
(Scan to add to calendar)
Abstract:
Abstract: Program invariants play an important useful role in understanding programs as well as verifying properties about them. There are many ways to obtain program invariants--automatically, semi-automatically or they could be provided by a programmer as a part of a specification of the program or as annotations. The problem of determining whether a proposed formula is an invariant is undecidable. In this talk, methods are proposed to determine when in certain cases, formulas expressed in various logical theories can be determined to be invariant. If a formula is indeed an invariant, techniques for strengthening the formula to generate inductive invariants are explored.
| Speaker: | Deepak Kapur (University of New Mexico Department of Computer Science School of Engineering Albuquerque, NM 87131-0001 United States of America) |
| Organiser: | Paritosh K Pandya |
| Date: | Friday, 21 Feb 2014, 16:00 to 17:30 |
| Venue: | D-405 (D-Block Seminar Room) |
(Scan to add to calendar)
Abstract:
Abstract: Program invariants play an important useful role in understanding programs as well as verifying properties about them. There are many ways to obtain program invariants--automatically, semi-automatically or they could be provided by a programmer as a part of a specification of the program or as annotations. The problem of determining whether a proposed formula is an invariant is undecidable. In this talk, methods are proposed to determine when in certain cases, formulas expressed in various logical theories can be determined to be invariant. If a formula is indeed an invariant, techniques for strengthening the formula to generate inductive invariants are explored.