Student research opportunities

Making Correct Programs Efficient

Project Code: CECS_1136

This project is available at the following levels:
CS single semester, Honours, Summer Scholar, Masters

Keywords:

Functional Programming, Program Extraction, Theorem Proving, Efficiency

Supervisor:

Dr Dirk Pattinson

Outline:

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 of this project

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/Prerequisites

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

Student Gain

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

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.

Contact: