Reference:

Rene Neumann. Using Promela in a fully verified executable LTL model checker. In Dimitra Giannakopoulou and Daniel Kroening, editors, Verified Software: Theories, Tools and Experiments, Lecture Notes in Computer Science, pages 105–114, July 2014.

Abstract:

In CAV2013 we presented an LTL model checker whose code has been completely verified using the Isabelle theorem prover. The intended use of the checker is to provide a trusted reference implementation against which more advanced checkers can be tested. However, in CAV2013 the checker still used an ad-hoc, primitive input language. In this paper we report on CAVA, a new version of the checker accepting inputs written in Promela. We report on our formalization of the Promela semantics within Isabelle, which is used both to define the semantics and to automatically generate code for the computation of the state space. We report on experiments on standard Promela benchmarks comparing our tool to SPIN.

Suggested BibTeX entry:

@inproceedings{VSTTE,
    author = {Rene Neumann},
    booktitle = {Verified Software: Theories, Tools and Experiments},
    editor = {Giannakopoulou, Dimitra and Kroening, Daniel},
    month = {July},
    pages = {105-114},
    series = {Lecture Notes in Computer Science},
    title = {Using {Promela} in a Fully Verified Executable {LTL} Model Checker},
    year = {2014}
}