Making Correct Programs Efficient

Research areas

Temporary Supervisor

Dr Dirk Pattinson

Description

The ``Correctness by Construction'' Paradigm extracts provably correct programs from proofs in a theorem prover. The price to pay for provable correctness is often execution speed as there are fewer opportunities for fine tuning. The aim of this project is to produce provably correct programs that can still handle real-world data. The target application is vote counting where correctness is paramount, but still millions of votes need to be counted efficiently.

Goals

We have already produced prototypes of vote counting programs using the ``Correctness by Construction'' paradigm. Goals are to investigate the performance bottlenecks alongside approaches to overcome them, while maintaining provable correctness.

Requirements

Interest in Functional Programming and/or Theorem Proving and/or Formal Methods

Background Literature

A case study that describes the generation of the vote counting programs is avaliable at http://users.cecs.anu.edu.au/~dpattinson/Software which contains instructions on how to build and run the case studies.

Gain

Hands-on experience in the area of software correctness and interactive theorem proving.

Updated:  1 June 2019/Responsible Officer:  Head of School/Page Contact:  CECS Marketing