Background:
Formal verification is essential to the correctness of software systems. When targeting systems of scale, verification efforts utilise frameworks comprising tools and techniques that streamline the proving process. These frameworks are typically tested using small case studies, ensuring their practicality prior to deployment. However, the lack of a comprehensive repository of examples can hinder this process, making it challenging to test and compare frameworks in an efficient manner.
Research Questions and Tasks:
This project aims to develop a repository of case studies for evaluating verification frameworks. This involves collating a diverse set of example systems, identifying their associated properties, and then formalising these systems and properties through suitable specification languages. The project will ideally be mechanised in a proof assistant, such as Isabelle/HOL.
Requirements:
A deep understanding of mathematical logic is a must. Students should also be familiar with programming language semantics, e.g. via COMP3610. Experience with formal methods is desirable but not required.