Alexander Schimpf, Stephan Merz, Jan-Georg Smaus. Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. Tobias Nipkow and Christian Urban.
22nd International Conference Theorem Proving in Higher-Order Logics - TPHOLs 2009, Aug 2009, Munich, Germany. Springer Berlin / Heidelberg, 5674, pp.424-439, 2009, Lecture Notes in Computer Science.
〈10.1007/978-3-642-03359-9_29〉.
〈inria-00408950〉