*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] New AFP entries: LTL Model Checker*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 29 May 2014 16:54:11 +0200*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.5.0

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 -------------------------------------------------------------------------------

- Previous by Date: Re: [isabelle] Rational functions
- Previous by Thread: Re: [isabelle] How to use transfer when lifting_forget has been called ?
- Cl-isabelle-users May 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list