The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
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. An approach based on solving recurrences will be presented. 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.