Benutzer: Gast  Login
Wenn Sie Schwierigkeiten haben, das Dokument zu öffnen, versuchen Sie auch bitte diesen Link
Originaltitel:
Formal Verification of Algorithms for Automata and Model Checking
Übersetzter Titel:
Formale Verifikation von Algorithmen für Automaten und Model Checking
Autor:
Brunner, Julian M.
Jahr:
2022
Dokumenttyp:
Dissertation
Fakultät/School:
TUM School of Computation, Information and Technology
Betreuer:
Nipkow, Tobias (Prof., Ph.D.)
Gutachter:
Nipkow, Tobias (Prof., Ph.D.); Esparza Estaun, Francisco Javier (Prof. Dr.)
Sprache:
en
Fachgebiet:
DAT Datenverarbeitung, Informatik
TU-Systematik:
DAT 706; DAT 540
Kurzfassung:
We verify algorithms and reference implementations using the proof assistant Isabelle. Firstly, we formalize an abstract, general, and extensible library for transition systems and automata. Secondly, we verify an ample set partial order reduction algorithm and integrate it into the CAVA model checker. Thirdly, we verify an algorithm for rank-based Büchi complementation and use it to implement a Büchi equivalence checker.
Übersetzte Kurzfassung:
Wir verifizieren Algorithmen und Referenzimplementierungen mit dem Beweisassistenten Isabelle. Erstens formalisieren wir eine abstrakte, generelle, und erweiterbare Bibliothek für Transitionssysteme und Automaten. Zweitens verifizieren wir einen Ample Set Partial Order Reduction Algorithmus und integrieren diesen in den CAVA Model Checker. Drittens verifizieren wir einen Algorithmus für Rang-basierte Büchi-Komplementierung und implementieren damit einen Büchi-Äquivalenzprüfer.
WWW:
https://mediatum.ub.tum.de/?id=1622049
Eingereicht am:
25.10.2021
Mündliche Prüfung:
19.12.2022
Dateigröße:
1884172 bytes
Seiten:
133
Urn (Zitierfähige URL):
https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20221219-1622049-1-5
Letzte Änderung:
12.04.2023
 BibTeX