Title:Imperative Programs on Numbers: Mechanization of Loop Invariant Generation and Loop Termination
Speaker: Deepak Kapur £¨Department of Computer Science University of New Mexico Albuquerque, NM USA£©
Time:10£º00am, Tuesday£¬July.8
Venue:Lecture Room,State Key Lab of Computer Science, Level
3 Building #5, Institute of Software, CAS
Abstract:
The talk will discuss recent research activities on two important aspects of
imperative programs operating on numbers.
A new approach for automatically generating polynomial equations as program
invariants from imperative programs will be presented. The focus will be on
the algebraic geometry methods, particularly how for a subclass of programs,
conjunctions of polynomial equations as invariants can be generated automatically
without knowing any input/output specification of a program.
Another heuristic based on quantifier elimination will also be presented. The
second property is that of loop termination.
By translating an imperative program to a constrained rewrite system, termination
techniques and tools from term rewriting literature are proposed for showing
termination of imperative programs working on numbers. Constraints are simple
number
theoretic relations on program variables, expressible in quantifier-free Presburger
arithmetic. A rewriting sequence is
proved to directly mimic computations of an imperative program. Termination
of such rewrite systems is shown by adapting
the dependency pair method and the associated dependency pair framework to the
constrained equational rewrite system modulo
Presburger arithmetic. The proposed approach has been used to prove termination
of a large class of imperative programs.
Bio of the speaker: