Benutzer: Gast  Login
Wenn Sie Schwierigkeiten haben, das Dokument zu öffnen, versuchen Sie auch bitte diesen Link
Originaltitel:
Verified Quantitative Analysis of Imperative Algorithms
Übersetzter Titel:
Verifizierte Quantitative Analyse von Imperativen Algorithmen
Autor:
Haslbeck, Maximilian Paul Louis
Jahr:
2021
Dokumenttyp:
Dissertation
Fakultät/School:
Fakultät für Informatik
Betreuer:
Nipkow, Tobias (Prof., Ph.D.)
Gutachter:
Nipkow, Tobias (Prof., Ph.D.); Hoffmann, Jan (Prof. Dr.)
Sprache:
en
Fachgebiet:
DAT Datenverarbeitung, Informatik
Stichworte:
Isabelle/HOL, Separation Logic, Algorithms, Refinement, Formal Verification, Running Time, Probabilistic Programs
Übersetzte Stichworte:
Isabelle/HOL, Separationslogik, Algorithmen, Verfeinerung, Formale Verifikation, Laufzeit, Probabilistische Programme
TU-Systematik:
DAT 706; DAT 540
Kurzfassung:
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.
Übersetzte Kurzfassung:
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
Eingereicht am:
22.02.2021
Mündliche Prüfung:
16.08.2021
Dateigröße:
1379528 bytes
Seiten:
229
Urn (Zitierfähige URL):
https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20210816-1596032-1-7
Letzte Änderung:
16.11.2021
 BibTeX