Imperative Programs on Numbers: Mechanization of Loop Invariant Generation and Loop Termination

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:
http://www.cs.unm.edu/~kapur/