Verifying Competitive-Programming Programs in a Rust Verifier
A big challenge in creating tasks for programming competitions such as external page ICPC and external page IOI is ensuring that the created master solutions are correct. While the task authors almost always provide an (informal) argument why a specific solution is correct, the correctness of the implementation is checked only by testing and peer-review.
Prusti is a verification tool for external page Rust programs developed in our group: it allows developers to write contracts and annotations in the source code, which are then automatically checked to prove functional correctness of the program. Internally, Prusti translates Rust programs to the Viper intermediate verification language. Since programs written in Rust have similar performance characteristics as the ones written in C and C++, Rust could be used as an alternative language to C and C++ in the programming competitions for writing master solutions.
Goals
The aim of this project is to find strategies for verifying correctness of certain classes of competitive programming tasks and to extend Prusti to support these strategies. The core milestones of this project are:
- Select several classes of solutions that would be amenable for verification (for example, greedy or dynamic programming) and collect a set of example problems from programming competitions that have solutions in the selected classes.
- Extend Prusti with features that are necessary for verifying the selected examples. We expect that most classes will require to implement support for Rust's slices (a contiguous sequence of elements in an array) and mathematical types such as sets, multisets, and sequences.
- Verify the collected examples.
- Describe strategies for verifying implementations of the selected classes.
Prerequisites
Since the project will require adapting and verifying many competitive programming exercise solutions, a good background in competitive programming is required.