LSV Seminar

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.

Past Seminars

The State of Inductive Theorem Proving for Software Verification

Tuesday, December 16 2008 at 11:00AM
Salle de Conférence (Pavillon des Jardins)
Lucas Dixon (University of Edinburgh)

Functional correctness for non-trivial properties of software requires inductive proof. Sadly this is an undecidable problem which typically requires frustrating amounts of user guidance. Fortunately, this makes it a fascinating topic for research; indeed, a significant strand of research considers heuristic approaches to inductive theorem proving, driven by syntactic observations. Recently, a type-theory based form of synthesis, combined with an upside-down twist on rewriting, has led to some exciting results. In this talk I will outline the state the field, give my view of the key intuitions for the emerging proof strategies, and highlight the exciting challenges currently being considered.

About LSV