CAVA LTL Modelchecker swMATH ID: 28830 Software Authors: Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf; Jan-Georg Smaus Description: CAVA_LTL_Modelchecker: A Fully Verified Executable LTL Model Checker. 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. An early version of this model checker is described in the CAV 2013 paper with the same title. Homepage: https://www.isa-afp.org/entries/CAVA_LTL_Modelchecker.html Related Software: Isabelle/HOL; Isabelle; Archive Formal Proofs; HOL; seL4; CakeML; Gabow SCC; Autoref; Coq; Locales; Isar; SPIN; CoSMed; FlowFox; Ur/Web; Jif; Isabelle/Isar; ML; Dijkstra Shortest Path; ConfiChair Cited in: 16 Publications all top 5 Cited by 27 Authors 5 Lammich, Peter 3 Popescu, Andrei 2 Bauereiß, Thomas 2 Pesenti Gritti, Armando 2 Raimondi, Franco 1 Abdulaziz, Mohammad 1 Aransay, Jesús 1 Brunner, Julian 1 Divasón, Jose 1 Dobrikov, Ivaylo 1 Esparza, Javier 1 Gretton, Charles 1 Griggio, Alberto 1 Hölzl, Johannes 1 Hou, Ping 1 Křetínský, Jan 1 Kunčar, Ondřej 1 Leuschel, Michael 1 Lochbihler, Andreas 1 Nipkow, Tobias 1 Norrish, Michael 1 Noschinski, Lars 1 Paulson, Lawrence Charles 1 Roveri, Marco 1 Sickert, Salomon 1 Tonetta, Stefano 1 Wenzel, Makarius Cited in 5 Serials 8 Journal of Automated Reasoning 2 Formal Aspects of Computing 2 Formal Methods in System Design 1 Journal of Functional Programming 1 Mathematics in Computer Science all top 5 Cited in 6 Fields 15 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) 1 Combinatorics (05-XX) 1 Probability theory and stochastic processes (60-XX) 1 Numerical analysis (65-XX) 1 Operations research, mathematical programming (90-XX) Citations by Year