Formally verifying some algorithm that has not yet been formally verified
The idea of this project is to take some algorithm (or data structure) and formally verify its functional correctness, i.e. that it always produces correct results. Ideally the project should do this for some algorithm that has not yet been formally verified.
One possibility might be to do this for A* search.
For a partial overview over what algorithms and data structures have been formally verified, see the following presentation slides due to Tobias Nipkow: http://www.mathematics.pitt.edu/hales60/pdf/Nipkow-Tobias.pdf.
The verification could for instance be carried out in Agda.
Contact: Nils Anders Danielsson