Seoul School on Isabelle/UTP
Dates: 17th - 21st July 2023
Location: Seoul National University, South Korea
This summer school course will train participants to apply Isabelle in assured software development. Isabelle harnesses techniques like functional programming, deductive proof, automated verification, and code generation. With Isabelle, we can subject models and programs to various analyses to find errors, and provide mathematical correctness proofs. Isabelle thus can be used to support assured model-based design and verification.
In the first part of the course, we will focus on functional specification. Students will first learn how to define abstract functional programs in HOL using algebraic datatypes and recursive functions. Then, we will look at proof in Isabelle/HOL, both in the form of natural deduction proof scripts and readable proofs using the Isar proof language. With these foundations in place, we will look at how to verify functional programs using techniques like case analysis, structural induction, and automated theorem proving.
In the second part, we will look at verifying imperative programs. We will introduce a simple abstract programming language, and the rules of Hoare logic in Isabelle. We will also look at the weakest preconditions calculus, which provides an equational proof method. We will then look at verification of imperative programs using verification condition generation and loop invariant annotations. Finally, time permitting, we will look at the Z Machine language, which is an abstract language for system-level modelling.
The course will be taught over 5 days. Half of the participants’ time will be spent in lectures, and the other half will be in problem-based learning classes, which will provide the opportunity for participants to apply the theoretical knowledge they have learned. Typically, these will be composed of Isabelle-based exercises, which will be tackled in teams, and then answers presented to the whole group afterwards. The lectures are all also accompanied by Isabelle-based theory documents, which serve as interactive lecture notes.
Dr Simon Foster is a lecturer in Computer Science at the University of York, and a member of the Software Engineering for Robotics group. He is an expert in interactive theorem proving using Isabelle/HOL, formal verification, and process algebra. Simon leads the development of Isabelle/UTP, a practical theorem prover forheterogeneous systems, which he has applied to verification of reactive and hybrid systems. He gained his PhD at the University of Sheffield in 2010 on a timed process algebra for Web services.