A Fully Verified Executable LTL Model Checker
| Autor: | Tobias Nipkow, Alexander Schimpf, René Neumann, Peter Lammich, Jan-Georg Smaus, Javier Esparza |
|---|---|
| Přispěvatelé: | Grélaud, Françoise, Centre National de la Recherche Scientifique - CNRS (FRANCE), Institut National Polytechnique de Toulouse - INPT (FRANCE), Technische Universität München - TUM (GERMANY), Université Toulouse III - Paul Sabatier - UT3 (FRANCE), Université Toulouse - Jean Jaurès - UT2J (FRANCE), Université Toulouse 1 Capitole - UT1 (FRANCE), Universität Freiburg (GERMANY), Institut de Recherche en Informatique de Toulouse - IRIT (Toulouse, France), Technische Universität Munchen - Université Technique de Munich [Munich, Allemagne] (TUM), University of Freiburg [Freiburg], Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, DFG grant CAVA, Computer Aided Verification of Automata, Institut für Informatik (LRR-TUM), Technische Universität München [München] (TUM), Archive of Formal Proofs, Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE) |
| Jazyk: | angličtina |
| Rok vydání: | 2016 |
| Předmět: |
Model checking
[INFO.INFO-AR]Computer Science [cs]/Hardware Architecture [cs.AR] interactive theorem proving Interactive theorem proving Computer science 0102 computer and information sciences 02 engineering and technology [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] [INFO] Computer Science [cs] computer.software_genre 01 natural sciences Interface homme-machine [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] Architectures Matérielles 0202 electrical engineering electronic engineering information engineering Code (cryptography) Génie logiciel [INFO]Computer Science [cs] [INFO.INFO-HC]Computer Science [cs]/Human-Computer Interaction [cs.HC] Reference implementation Pseudocode Functional programming Programming language Proof assistant 020207 software engineering computer.file_format Modélisation et simulation [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation Systèmes embarqués Automated theorem proving 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Cryptographie et sécurité [INFO.INFO-ES]Computer Science [cs]/Embedded Systems Executable Isabelle computer LTL |
| Zdroj: | Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 25th International Conference on Computer Aided Verification (CAV 2013) 25th International Conference on Computer Aided Verification (CAV 2013), Jun 2013, Saint Petersbourg, Russia. pp.463-478, ⟨10.1007/978-3-642-39799-8_31⟩ [Research Report] Archive of Formal Proofs. 2016 Computer Aided Verification ISBN: 9783642397981 CAV |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|