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.
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.
Interest in Functional Programming and/or Theorem Proving and/or Formal Methods
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.
Hands-on experience in the area of software correctness and interactive theorem proving.