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.