A Fully Verified Executable LTL Model Checker (Q7361160)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry CAVA_LTL_Modelchecker
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | A Fully Verified Executable LTL Model Checker |
AFP entry CAVA_LTL_Modelchecker |
Statements
28 May 2014
0 references
Javier Esparza
0 references
Peter Lammich
0 references
René Neumann
0 references
Tobias Nipkow
0 references
Alexander Schimpf
0 references
Jan-Georg Smaus
0 references
A Fully Verified Executable LTL Model Checker (English)
0 references
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.
0 references
