From EECS

Abstract

An overview of the recent work in our group on automatic generation of loop invariants using different approaches will be presented. Particularly, a heuristic based on quantifier-elimination will be reviewed. Methods based on abstract interpretation and ideal-theoretic semantics of programming language constructs will be discussed. These methods have been implemented and successfully tried on many programs implementing nontrivial number theoretic functions. Some preliminary ideas about how to generalize these approaches to work on data types other than numbers will be discussed.