Benutzer: Gast  Login
Originaltitel:
CAVA – A Verified Model Checker 
Übersetzter Titel:
CAVA - Ein verifizierter Modelchecker 
Jahr:
2017 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.) 
Gutachter:
Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.); Nipkow, Tobias (Prof., Ph.D.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
TU-Systematik:
DAT 500d 
Kurzfassung:
Model checkers like SPIN provide a way to gain certainty about the behavior of programs and protocols. To guarantee that the model checker itself is correct, the CAVA project developed a verified and executable LTL model checker using Isabelle/HOL.
This thesis reports on various building blocks of CAVA by presenting the first formalized and executable Promela semantics, a framework for verifying depth-first search based algorithms, and an automata library. As a part thereof, this thesis will deta...    »
 
Übersetzte Kurzfassung:
Modelchecker, wie z.B. SPIN, sind eine Möglichkeit, Gewissheit über das Verhalten von Programmen und Protokollen zu erlangen. Um nun sicherzustellen, dass der Modelchecker selber korrekt ist, wurde im Projekt CAVA ein verifizierter und ausführbarer Modelchecker mit Hilfe von Isabelle/HOL entwickelt.
In dieser Dissertation stellen wir verschiedene Bausteine von CAVA vor: Die erste formalisierte und ausführbare Semantik von Promela, ein Framework um auf Tiefensuche basierende Algorithmen zu verifiz...    »
 
Mündliche Prüfung:
16.06.2017 
Dateigröße:
1371277 bytes 
Seiten:
141 
Letzte Änderung:
06.07.2017