User: Guest  Login
Original title:
CAVA – A Verified Model Checker 
Translated title:
CAVA - Ein verifizierter Modelchecker 
Year:
2017 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.) 
Referee:
Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.); Nipkow, Tobias (Prof., Ph.D.) 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
TUM classification:
DAT 500d 
Abstract:
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...    »
 
Translated abstract:
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...    »
 
Oral examination:
16.06.2017 
File size:
1371277 bytes 
Pages:
141 
Last change:
06.07.2017