@inproceedings{e8ee6660cab44225b031a61283f96194,
title = "Verifying the LTL to B{\"u}chi Automata Translation via Very Weak Alternating Automata",
abstract = "We present a formalization of a translation from LTL formulae to generalized B{\"u}chi automata in the HOL4 theorem prover. Translations from temporal logics to automata are at the core of model checking algorithms based on automata-theoretic techniques. The translation we verify proceeds in two steps: it produces very weak alternating automata at an intermediate stage, and then ultimately produces a generalized B{\"u}chi automaton. After verifying both transformations, we also encode both of these automata models using a generic, functional graph type, and use the CakeML compiler to generate fully verified machine code implementing the translation.",
author = "Simon Jantsch and Michael Norrish",
note = "Publisher Copyright: {\textcopyright} 2018, Springer International Publishing AG, part of Springer Nature.; 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018 ; Conference date: 09-07-2018 Through 12-07-2018",
year = "2018",
doi = "10.1007/978-3-319-94821-8\_18",
language = "English",
isbn = "9783319948201",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "306--323",
editor = "Jeremy Avigad and Assia Mahboubi",
booktitle = "Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings",
address = "Germany",
}