User: Guest  Login
If you experience problems opening the document, please try this link.
Original title:
Formal Verification of Algorithms for Automata and Model Checking
Translated title:
Formale Verifikation von Algorithmen für Automaten und Model Checking
Author:
Brunner, Julian M.
Year:
2022
Document type:
Dissertation
Faculty/School:
TUM School of Computation, Information and Technology
Advisor:
Nipkow, Tobias (Prof., Ph.D.)
Referee:
Nipkow, Tobias (Prof., Ph.D.); Esparza Estaun, Francisco Javier (Prof. Dr.)
Language:
en
Subject group:
DAT Datenverarbeitung, Informatik
TUM classification:
DAT 706; DAT 540
Abstract:
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.
Translated abstract:
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
Date of submission:
25.10.2021
Oral examination:
19.12.2022
File size:
1884172 bytes
Pages:
133
Urn (citeable URL):
https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20221219-1622049-1-5
Last change:
12.04.2023
 BibTeX