When is a Formula Invariant?


Deepak Kapur


University of New Mexico
Department of Computer Science
School of Engineering
Albuquerque, NM 87131-0001
United States of America


Friday, 21 February 2014, 16:00 to 17:30



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.