News Archives

Automatic Generation of Loop Invariants

November 23, 2004

Date: Tuesday November 23, 2004
Time: 11am-12:15pm
Location: Woodward 149

Deepak Kapur <>

I will start with a bird's eye-view of my research activities. I will then switch to a research problem I have been working on during the last year -- automatic generation of loop invariants. Three different but related approaches developed in collaboration with Enric Rodriguez-Carbonell will be presented. The critical role of algebraic geometry in discovering these results will be discussed. It is proposed that equally rich theories about other data structures will have to be developed in order to make progress in automatically generating program invariants expressed in terms of properties of such data structures.