Andrew Butterfield

My research interests are mainly in the area of software modelling and verification using mathematical logic to reason about program behaviour and correctness (a.k.a. formal methods). I am also keen user of functional programming languages as a basis for building tool support. I am very happy to supervise projects in formal methods, involving any programming language (even Java!), or projects using functional languages to implement applications in general (not just limited to formal methods). In 2019/2020 in am involved in a multi-partner project funded by the European Space Agency looking at the formal verification of critical parts of an open-source operating system (rtems.org). There will be opportunites for final-year/MCS projects to be scoped around this activity.

Using Promela/SPIN to verify lightweight operating systems for Cubesats

Andrew Butterfield (email | all projects)

Cubesats are small satellites that are built as on ore more 10cm-sized cubes. There is a growing industry for developing and launching these. Typically their computing requirements are relatively low, and so they often use lightweight versions of operating systems. This project looks at using Promela/SPIN to model and do test generation for some key … Read more

Using Promela/SPIN to verify RTEMS

Andrew Butterfield (email | all projects)

RTEMS (https://www.rtems.org/) is an open-source real-time operating system widely used in aircraft and spacecraft. It offers a comprehensive API, mostly defined in terms of “managers” that provide calls to perform specific kinds of services or provide specific infrastructure. As part of an activity sponsored by the European Space Agency (ESA) we have developed a methodology … Read more

Enhancing a Theorem Prover written in Haskell

Andrew Butterfield (email | all projects)

A theorem prover “reasonEq” , written in Haskell, is currently under development. It is intended to support reasoning about the meaning and correctness of programs. It supports an easy to use proof style for predicate calculus known as “equational reasoning” – very similar to the kind of algebraic reasoning used in most mathematics found in … Read more

Domain-Specific Languages in Haskell

Andrew Butterfield (email | all projects)

Haskell (haskell.org) is good for developing Domain Specific Languages (DSLs). A classic example of this are financial combinators – the linked paper led to a financial services spinout (lexifi.com) that is still going strong. There is an interesting overview of using Haskell to design DSLs. I am always willing to supervise projects in this space. … Read more