OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

A Fully Verified Executable LTL Model Checker

Esparza, Javier and Lammich, Peter and Neumann, René and Nipkow, Tobias and Schimpf, Alexander and Smaus, Jan-Georg A Fully Verified Executable LTL Model Checker. (2013) In: 25th International Conference on Computer Aided Verification (CAV 2013), 13 June 2013 - 19 July 2013 (Saint Petersbourg, Russian Federation).

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
266kB

Official URL: http://dx.doi.org/10.1007/978-3-642-39799-8_31

Abstract

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 recent Isabelle technology called the 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. We report on the structure of the checker, the development process, and some experiments on standard benchmarks.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer editor. This papers appears in Volume 8044 Lecture Notes in Computer Science ISSN : 0302-9743. ISBN: 978-3-642-39798-1. The original PDF is available at : http://link.springer.com/chapter/10.1007%2F978-3-642-39799-8_31
HAL Id:hal-01226469
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
Other partners > Technische Universität München - TUM (GERMANY)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > Universität Freiburg (GERMANY)
Laboratory name:
Statistics:download
Deposited By: IRIT IRIT
Deposited On:13 Oct 2015 09:05

Repository Staff Only: item control page