Workshop on inductive theorem proving
Saturday 23rd & Sunday 24th November 2013
Imperial College London
Department of Computing,
180 Queen’s Gate
This workshop will be very informal and simply aim to give researchers interested in inductive theorem a chance to meet and exchange ideas. We hope for a lot of interaction between participants and an opportunity to actually try out some of the available theorem provers.
9.30 - 10.00
Welcome and introduction. Participants briefly say a few words on what their interests are and what they hope to get from the workshop.
10.00 - 10.45 Demo of the Dafny system, Rustan Leino
10.45 - 11.30 Using Dafny in Teaching, Sophia Drossopoulou
11.30- 12.00 Zeno - a retrospective look, Will Sonnex
12.00 - 13.30 Lunch
15.00-15.30 Coffe Break
Discussion of new opportunities
Please feel free to suggest topics of interest that spring to mind on the day. Some topics to consider are:
- What can we do to combine the good features of the various tools?
- Creation of a shared benchmark suit for inductive provers?
Gather at a pub for those who wish, then out for dinner.
10.15 - 10.45 Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models, Koen Claessen
10.45 - 11.05 Coffe break
11.05 - 11.25 Theory Exploration for Interactive Theorem Provers, Moa Johansson
11.25 - 12.20 Making explicit the implicit induction, Sorin Stratulat
12.30 - 14.00 Lunch
15.00 End of workshop
Note that there are engineering works on parts of the tube network and also on the trainline to Stanstead airport which might add to journey times.
Please email Sophia Drossopoulou if you want to participate and have not yet registered.