From 20 May 2019 the CPS Lab will organize a Tutorial Week on Isabelle/HOL with two guest experts from UK. You are all invited; student, researcher, or practitioner from industry. (Pizza for lunch!)
Come, listen, play with Isabelle, and have lunch with us!
Official
Title: Isabelle/HOL for Program Correctness: A Beginner's Guide
Description.
Isabelle/HOL is one of the most popular proof assistants. It allows the specification of mathematical and computational models in a formal language and provides tools for performing mathematical proofs about them. What sets Isabelle/HOL apart from similar tools is its balance between the expressivity of its specification language and the degree of automation of its solvers and theorem provers. This makes it particularly suitable for the analysis and verification of programs and computing systems. There is in fact a large and dynamic user community in these fields. Particular Isabelle success stories are the seL4 microkernel verification and the formal proof of the Kepler conjecture in mathematics.
This mini-course starts with a gentle introduction to Isabelle/HOL: an overview of its user interface and proof IDE, a survey of the main features of its specification language, a classical higher-order logic that ressembles a functional programming language, and a demonstration of its solvers, theorem provers, counterexample generators and proof scripting languages. Then we learn how to do proofs at different levels of complexity, from logical and equational reasoning to proofs by cases and induction, how to define and use types and data types such as trees and functional lists, and how to define and reason with simple algebraic structures by using axiomatic type classes.
In the second part of the course we apply these techniques to the formalisation of simple program verification and program construction tools based on Hoare logic and predicate transformers. We mainly use a denotational relational semantics for this, but also discuss how structural operational semantics can be formalised.
If time permits and the audience is interested, we can have glimpse at more advanced applications, such as formalisations of a differential dynamic logic for the verification of hybrid systems.
Plan: 2h lectures > Lunch break > 1h Exercises.
The course is delivered as five blocks that consist in two hours of lectures in the morning and one hour of exercise sessions in the afternoon. The lectures themselves are meant to be highly interactive, and there is a certain flexibility to adapt them to interest. It is desirable that participants bring their own laptops to lectures and exercise sessions. Instructions on how to install Isabelle will be provided at the beginning of the course. They can also be found online: https://isabelle.in.tum.de/index.html
Program (from Monday 20 May to Friday 24 May)
- Monday (beginners) 5th floor
- 10:00 Lecture (Jonathan) (files: overview.pdf )
- 12:00 Lunch (Pizza for everyone, even vegetarian)
- 13:00 Exercises hour (interactions with tutors possible also afterwards)
(files: day1.thy , day1_extras.thy , exercise-1.pdf)
- Tuesday (beginners) 5th floor
! earlier start due to Abel Prize ceremony !- 9:30 Lecture (Jonathan)
- 11:30 Lunch
- 12:30 Exercises hour (files: day2.thy , exercise-2.pdf)
- Wednesday (intermediate) 8th floor
- 10:00 Lecture (Jonathan/Georg) (files: isaver.pdf )
- 12:00 Lunch break
- 13:00 Exercises hour (files: day3.thy , language_ka_empty.thy , locale_kat_empty.thy , verification_kat_empty.thy , exercise-3.pdf)
- Thursday (intermediate) 8th floor
- 10:00 Lecture (Georg)
- 12:00 Lunch break
- 13:00 Exercises hour (files: exercise-4.pdf)
- Friday (advanced) 8th floor
- 10:00 Lecture (Georg)
- 12:00 Lunch break
- 13:00 Exercises hour (files: exercise-5.pdf)
Logistics
The tutorial takes place in the Informatics (IFI) building called Ole-Johan Dahls Hus in the Blindern campus of the University of Oslo.
We suggest to take from centre the metro lines 4 or 5 in the direction West and stop at Forskningsparken.
From here walk under the metro-line-bridge to reach the big black building. This should be visible from the metro station.
Enter in the tower part D, and take lift to 5/8th floor. We might change the room depending on the number of participants. Look for our poster on the door. Monday and Tuesday we have booked the room 5470/8459.
Wifi Networks:
- UiO guest (browser login info)
- Eduroam
Registration
Possible Homework topics (not part of Exercises sessions)
The following are possible suggestions of topics that participants can take, either in groups or individually, and try out the acquired knowledge, on some more challenging tasks. These are not part of the Exercise sessions. Talk first with the tutors. Suggest other complex topics.
- Synchronous Kleene Algebra in Isabelle (similar to the works of Georg)
- Dynamic Structural Operational Semantics in Isabelle (or some part of it like Modular SOS or Encapsulation for concurrent objects)
- Pomsets in Isabelle
- Synthesis of programs (proofs like correctness or completeness) in Isabelle