140x Filetype PDF File size 0.61 MB Source: ethz.ch
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
no reviews yet
Please Login to review.