When is a formula invariant?
Title: When is a formula invariant?
Speaker: Deepak Kapur (Univ. of New Mexico, USA)
Time: 11:30-12:00, Thursday, 28th November, 2013.
Venue: Lecture Room, 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
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.
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.