{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T16:26:08Z","timestamp":1725812768576},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662458235"},{"type":"electronic","value":"9783662458242"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-45824-2_11","type":"book-chapter","created":{"date-parts":[[2014,12,1]],"date-time":"2014-12-01T06:07:51Z","timestamp":1417414071000},"page":"158-169","source":"Crossref","is-referenced-by-count":1,"title":["B\u00fcchi Automata Optimisations Formalised in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Schimpf","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan-Georg","family":"Smaus","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, 5th print. MIT Press (2002)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-39799-8_31","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2013","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 463\u2013478. Springer, Heidelberg (2013)"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-44618-4_13","volume-title":"CONCUR 2000 - Concurrency Theory","author":"K. Etessami","year":"2000","unstructured":"Etessami, K., Holzmann, G.J.: Optimizing B\u00fcchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 153\u2013167. Springer, Heidelberg (2000)"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembinski, P., Sredniawa, M. (eds.) Proceedings of the 15th International Symposium on Protocol Specification, Testing, and Verification. IFIP Conference Proceedings, vol.\u00a038, pp. 3\u201318. Chapman and Hall (1996)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"11_CR5","unstructured":"Holzmann, G.J.: The SPIN Model Checker - primer and reference manual. Addison-Wesley (2004)"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-32347-8_12","volume-title":"Interactive Theorem Proving","author":"P. Lammich","year":"2012","unstructured":"Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft\u2019s algorithm. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 166\u2013182. Springer, Heidelberg (2012)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-642-03359-9_29","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Schimpf","year":"2009","unstructured":"Schimpf, A., Merz, S., Smaus, J.-G.: Construction of B\u00fcchi automata for LTL model checking verified in Isabelle\/HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 424\u2013439. Springer, Heidelberg (2009)"},{"issue":"2","key":"11_CR9","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R.E. Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput.\u00a01(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B), pp. 133\u2013192. Elsevier and MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50009-3"}],"container-title":["Lecture Notes in Computer Science","Logic and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-45824-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T16:39:37Z","timestamp":1559061577000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-45824-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662458235","9783662458242"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-45824-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}