Workshop on inductive theorem proving

Saturday 23rd  & Sunday 24th November 2013

Imperial College London

 

Department of Computing,

180 Queen’s Gate

Room 217/218

 

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.

 

 Saturday 23/11

 

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

 

13.30 -14.15  HipSpec: Automating Inductive Proofs using Theory Exploration,  Dan Rosen

 

14.15 - 15.00  Automated functional program verification using fixpoint fusion, Will Sonnex

 

15.00-15.30 Coffe Break 

 

15.30

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?

 

(around) 18.00 

Gather at a pub for those who wish, then out for dinner.

 

 

Sunday 24/11

 

09.30 - 10.15 Cyclic Abduction of Inductive Safety & Termination Preconditions, James Brotherston 

 

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

 

14.00 - 14.45,  Verifying Turing machine programs in Isabelle, Christian Urban

 

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.