Verified LTL to Büchi in HOL

In this talk I present a translation from LTL formulae to Büchi automata that uses weak alternating automata as an intermediate result. In many cases this translation gives better results than the classic tableaux approach. I discuss a correctness proof of the translation and my work on formalising it in the HOL theorem prover. Then I ddress the problem of bridging the gap between an abstract and a concrete implementation and how we can use the CakeML compiler to solve it.

Date & time

3–4pm 21 Sep 2017


Room:N224 Computer Systems shared space


Simon Jantsch


Updated:  10 August 2021/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing