Email Gateway (Aug 19 2022 at 14:24): Email Gateway (Aug 19 2022 at 14:24):From: Tobias Nipkow <nipkow@in.tum.de>
Below you find 5 new entries, the components of an exceutable and reasonably
efficient LTL Model Checker. The last entry combines them all. An early version
was described in a CAV 2013 paper: http://www.in.tum.de/~nipkow/pubs/cav13.html
The CAVA Automata Library
Peter Lammich
We report on the graph and automata library that is used in the fully verified
LTL model checker CAVA. As most components of CAVA use some type of graphs or
automata, a common automata library simplifies assembly of the components and
reduces redundancy.
The CAVA Automata Library provides a hierarchy of graph and automata classes,
together with some standard algorithms. Its object oriented design allows for
sharing of algorithms, theorems, and implementations between its classes, and
also simplifies extensions of the library. Moreover, it is integrated into the
Automatic Refinement Framework, supporting automatic refinement of the abstract
automata types to efficient data structures.
Note that the CAVA Automata Library is work in progress. Currently, it is very
specifically tailored towards the requirements of the CAVA model checker.
Nevertheless, the formalization techniques presented here allow an extension of
the library to a wider scope. Moreover, they are not limited to graph libraries,
but apply to class hierarchies in general.
The CAVA Automata Library is described in the paper: Peter Lammich, The CAVA
Automata Library, Isabelle Workshop 2014, to appear.
http://afp.sourceforge.net/entries/CAVA_Automata.shtml
Converting Linear-Time Temporal Logic to Generalized Büchi Automata
Alexander Schimpf and Peter Lammich
We formalize linear-time temporal logic (LTL) and the algorithm by Gerth et al.
to convert LTL formulas to generalized Büchi automata. We also formalize some
syntactic rewrite rules that can be applied to optimize the LTL formula before
conversion. Moreover, we integrate the Stuttering Equivalence AFP-Entry by
Stefan Merz, adapting the lemma that next-free LTL formula cannot distinguish
between stuttering equivalent runs to our setting.
We use the Isabelle Refinement and Collection framework, as well as the Autoref
tool, to obtain a refined version of our algorithm, from which efficiently
executable code can be extracted.
http://afp.sourceforge.net/entries/LTL_to_GBA.shtml
Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm
Peter Lammich
We present an Isabelle/HOL formalization of Gabow's algorithm for finding the
strongly connected components of a directed graph. Using data refinement
techniques, we extract efficient code that performs comparable to a reference
implementation in Java. Our style of formalization allows for re-using large
parts of the proofs when defining variants of the algorithm. We demonstrate this
by verifying an algorithm for the emptiness check of generalized Büchi
automata, re-using most of the existing proofs.
http://afp.sourceforge.net/entries/Gabow_SCC.shtml
Promela Formalization
René Neumann
We present an executable formalization of the language Promela, the description
language for models of the model checker SPIN. This formalization is part of the
work for a completely verified model checker (CAVA), but also serves as a useful
(and executable!) description of the semantics of the language itself, something
that is currently missing. The formalization uses three steps: It takes an
abstract syntax tree generated from an SML parser, removes syntactic sugar and
enriches it with type information. This further gets translated into a
transition system, on which the semantic engine (read: successor function) operates.
http://afp.sourceforge.net/entries/Promela.shtml
A Fully Verified Executable LTL Model Checker
Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf,
Jan-Georg Smaus
We present an LTL model checker whose code has been completely verified using
the Isabelle theorem prover. The checker consists of over 4000 lines of ML code.
The code is produced using the Isabelle Refinement Framework, which allows us to
split its correctness proof into (1) the proof of an abstract version of the
checker, consisting of a few hundred lines of ``formalized pseudocode'', and (2)
a verified refinement step in which mathematical sets and other abstract
structures are replaced by implementations of efficient structures like
red-black trees and functional arrays. This leads to a checker that, while still
slower than unverified checkers, can already be used as a trusted reference
implementation against which advanced implementations can be tested.
http://afp.sourceforge.net/entries/CAVA_LTL_Modelchecker.shtml
Last updated: Apr 20 2024 at 08:16 UTC