Verified Quantitative Analysis of Imperative Algorithms

Haslbeck, Maximilian Paul Louis

User: Guest

Maximilian Paul Louis Haslbeck

If you experience problems opening the document, please try this link.

Original title:: Verified Quantitative Analysis of Imperative Algorithms
Translated title:: Verifizierte Quantitative Analyse von Imperativen Algorithmen
Author:: Haslbeck, Maximilian Paul Louis
Year:: 2021
Document type:: Dissertation
Faculty/School:: Fakultät für Informatik
Advisor:: Nipkow, Tobias (Prof., Ph.D.)
Referee:: Nipkow, Tobias (Prof., Ph.D.); Hoffmann, Jan (Prof. Dr.)
Language:: en
Subject group:: DAT Datenverarbeitung, Informatik
Keywords:: Isabelle/HOL, Separation Logic, Algorithms, Refinement, Formal Verification, Running Time, Probabilistic Programs
Translated keywords:: Isabelle/HOL, Separationslogik, Algorithmen, Verfeinerung, Formale Verifikation, Laufzeit, Probabilistische Programme
TUM classification:: DAT 706; DAT 540
Abstract:: This thesis applies formal verification to the running time analysis of algorithms. First, three Hoare logics for time bounds from the literature are studied and their application to probabilistic programs is explored. Then, a practical framework using Separation Logic with Time Credits is presented. Finally, stepwise refinement is extended to reason about the resource usage of programs. The theory is applied to formally verify the running time of introspection sort and Kruskal‘s algorithm.
Translated abstract:: Diese Dissertation wendet formale Verifikation auf die Laufzeitanalyse von Algorithmen an. Zuerst werden drei Hoare Logiken für Laufzeitschranken untersucht und ihre Anwendung auf probabilistische Programme erkundet. Dann wird ein konkretes Werkzeug basierend auf Separationslogik mit Time Credits realisiert und die Technik Schrittweise Verfeinerung auf Laufzeitanalyse erweitert. Mithilfe der entwickelten Werkzeuge wird die Laufzeitanalyse von Introsort und Kruskal‘s Algorithmus verifiziert.
WWW:: https://mediatum.ub.tum.de/?id=1596032
Date of submission:: 22.02.2021
Oral examination:: 16.08.2021
File size:: 1379528 bytes
Pages:: 229
Urn (citeable URL):: https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20210816-1596032-1-7
Last change:: 16.11.2021
BibTeX