User: Guest  Login
Original title:
Verified Quantitative Analysis of Imperative Algorithms 
Translated title:
Verifizierte Quantitative Analyse von Imperativen Algorithmen 
Year:
2021 
Document type:
Dissertation 
Institution:
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. 
Oral examination:
16.08.2021 
File size:
1379528 bytes 
Pages:
229 
Last change:
16.11.2021