DEPARTMENTOFINFORMATICS
                    TECHNISCHEUNIVERSITÄTMÜNCHEN
                      Master’s Thesis in Informatics
        Verifying Competitive-Programming Programs
                       in a Rust Verifier
                          AhmedRayan
                           DEPARTMENTOFINFORMATICS
                                    TECHNISCHEUNIVERSITÄTMÜNCHEN
                                        Master’s Thesis in Informatics
               Verifying Competitive-Programming Programs
                                            in a Rust Verifier
                           Verifizierung von Programmen aus
                     Competitive Programming in einem Rust
                                                    Verifier
                             Author:            AhmedRayan
                             Supervisor:        Prof. Dr. Susanne Albers
                             Advisor:           Vytautas Astrauskas, Prof. Dr. Peter Müller
                             Submission Date:   15.04.2021
       I confirm that this master’s thesis in informatics is my own work and I have documented all
       sources and material used.
       Munich, 15.04.2021     AhmedRayan
        Abstract
        Ensuring the correctness of the created master solutions is one of the biggest challenges
        that people face in creating tasks for programming competitions such as ICPC and IOI. The
        task authors usually check the solutions’ correctness by testing or peer review. However,
        that doesn’t give sure guarantees on the solutions’ correctness. In this thesis, we explore
        an alternative way to do that by using Prusti to formally verify the correctness of the Rust
        implementation to these master solutions. We investigate if we can find a general strategy to
        verify the solutions’ correctness of the tasks belonging to each of the following competitive
        programming topics: Dynamic Programming (DP), DP on Trees, Greedy, and Segment Tree.
        Unlike the already existing published papers and archives that contain verification for the
        correctness of specific algorithms using other tools, we explore general strategies for whole
        classes of problems.
                               iii