Click here for Details.
We proudly present the Isabelle Summer School at MDX funded by the Faculty
of Science and Technology.
Isabelle is an interactive theorem prover that has long been recognized and
established as one of the best of its kind with numerous applications both
in academia and industry. One of its major success stories is application for
the verification of security of operating systems like seL4. Apple uses it for
the analysis of IOS and Intel for RISC-V ISA (Instruction Set Architecture)
verification.
The Isabelle MDX Summer School takes place at Middlesex University London
from 26.-30. June 2023 in Hendon (Public) Library room HL119.
The summer school offers an expert led introduction to practical
working with Isabelle and how to apply it to model and analyse state based
computing systems like IOS and ISA.
Participation is free but places are limited so only a selected number of
participants can be admitted.
A small number of industrially funded MDX internship projects and one funded
PhD-ship are planned as follow-ups of the summer school.
The summer school is primarily addressed to students (final year BSc CS/IT/Math, MSc
and postgraduate researchers in CS, IT, Math) as it starts in the first couple of days
with a hands-on introduction to working with Isabelle.
However, the summer school is also open for interested staff members who might consider
joining in mainly for the second half of the week presenting invited expert talks on the
specific subjects of integrsation of AI and SMT solvers and application to ISA verification.
Please email a comprehensive expression of interest of participation to the
convenor Dr Florian Kammueller (f.kammueller@mdx.ac.uk)
Click here for Timetable
There are 6 sessions a 45 min a day between 10 am and 4 pm with coffee and lunch breaks.
The sessions are organized in double sessions A, B, C consisting of 90 minutes (2x45minutes).
The summer school does not request any previous knowledge of Isabelle or interactive theorem proving
but a general understanding of logic.
Timetable
Mo 26.6.2023
A. Introduction to Isabelle, Terms and Types (Florian Kammueller)
B. Declarative Proofs in Isabelle with Isar (Nadine Karsten, TU Berlin)
C. Logic and Deduction (Florian Kammueller)
Tu 27.6.2023
A. Basic Interaction with Isabelle (Florian Kammueller)
B. Sets and Predicates (Nadine Karsten, TU Berlin)
C. Induction, Proof automation (Nadine Karsten, TU Berlin)
We 28.6.2023
A. Introduction to the Isabelle challenge (Nadine Karsten)
B. Isabelle Lab session: Practical working on the challenge (Nadine Karsten, F. Kammueller)
C. Integrating SMT solving into Isabelle (Mathias Fleury, Univ Freiburg, Germany)
Th 29.6.2023
A. Integrating SMT solving into Isabelle (Mathias Fleury, Univ Freiburg, Germany)
B. Isabelle Lab session: Practical working on the challenge (Nadine Karsten, F. Kammueller)
C. Security Engineering with Isabelle (Florian Kammueller)
Fr 30.6.2023
A. Isabelle Challenge evaluation (Florian Kammueller)
B. ISA verification in Isabelle: Sail and the Morello verfication (Thomas Bauereiss, Univ. of Cambridge)
C. Isabelle for OS and C verification and ML automation (Thomas Sewell, University of Cambridge)