Case Studies for Formal Methods

formal methods, formal modelling

Picture of Peter Hoefner

11 Jun 2024

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.

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.

You are on Aboriginal land.

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

arrow-left bars search times