Seoul School on Isabelle/UTP

Dates: 17th - 21st July 2023

Location: Seoul National University, South Korea

Course Content

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.

Structure

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.

Participation

The summer school will take place at Seoul National University in the College of Engineering Building 302. You can register for the school through the following link. For more local information, please contact Prof. Chung-Kil Hur.