@InProceedings{schimpf:construction, author = {Alexander Schimpf and Stephan Merz and Jan-Georg Smaus}, title = {Construction of {B\"uchi} Automata for {LTL} Model Checking Verified in {I}sabelle/{HOL}}, booktitle = {22nd Intl. Conf. Theorem Proving in Higher-Order Logics (TPHOLs 2009)}, pages = {424-439}, year = 2009, editor = {Tobias Nipkow and Christian Urban}, volume = 5674, series = {Lecture Notes in Computer Science}, address = {Munich, Germany}, publisher = {Springer}, }