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 



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.