{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T22:54:46Z","timestamp":1742943286925,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319406473"},{"type":"electronic","value":"9783319406480"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40648-0_23","type":"book-chapter","created":{"date-parts":[[2016,6,3]],"date-time":"2016-06-03T09:42:13Z","timestamp":1464946933000},"page":"307-321","source":"Crossref","is-referenced-by-count":6,"title":["Formal Verification of an Executable LTL Model Checker with Partial Order Reduction"],"prefix":"10.1007","author":[{"given":"Julian","family":"Brunner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Lammich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,4]]},"reference":[{"key":"23_CR1","series-title":"Graduate Texts in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"RJ Back","year":"1998","unstructured":"Back, R.J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, Heidelberg (1998)"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-319-08970-6_7","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93\u2013110. Springer, Heidelberg (2014)"},{"key":"23_CR3","unstructured":"Brunner, J.: Implementation and Verification of Partial Order Reduction for On-The-Fly Model Checking. MA thesis. Technische Universit\u00e4t M\u00fcnchen, 83 p., 15 July 2014. http:\/\/www21.in.tum.de\/brunnerj\/documents\/ivporotfmc.pdf"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/3-540-61042-1_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"CT Chou","year":"1996","unstructured":"Chou, C.T., Peled, D.: Formal verification of a partial-order reduction technique for model checking. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 241\u2013257. Springer, Heidelberg (1996)"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 8044, pp. 463\u2013478. Springer, Heidelberg (2013)"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.G.: A fully verified executable LTL model checker. Archive of Formal Proofs, May 2014. http:\/\/afp.sf.net\/entries\/CAVA_LTL_Modelchecker.shtml , formal proof development","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"23_CR7","unstructured":"Holzmann, G.J.: The SPIN Model Checker. Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)"},{"key":"23_CR8","unstructured":"Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: SPIN Workshop, vol. 32, pp. 81\u201389 (1996)"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1007\/BFb0054182","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"RP Kurshan","year":"1998","unstructured":"Kurshan, R.P., Levin, V., Minea, M., Peled, D.A., Yenig\u00fcn, H.: Static partial order reduction. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 345\u2013357. Springer, Heidelberg (1998)"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/978-3-319-08970-6_21","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2014","unstructured":"Lammich, P.: Verified efficient implementation of Gabow\u2019s strongly connected component algorithm. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 325\u2013340. Springer, Heidelberg (2014)"},{"key":"23_CR11","unstructured":"Lammich, P.: Collections framework. Archive of Formal Proofs, November 2009. http:\/\/afp.sf.net\/entries\/Collections.shtml , formal proof development"},{"key":"23_CR12","unstructured":"Lammich, P.: Refinement for monadic programs. Archive of Formal Proofs, January 2012. http:\/\/afp.sf.net\/entries\/Refine_Monadic.shtml , formal proof development"},{"key":"23_CR13","unstructured":"Lammich, P.: The CAVA automata library. Archive of Formal Proofs, May 2014. http:\/\/afp.sf.net\/entries\/CAVA_Automata.shtml , formal proof development"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/978-3-319-22102-1_17","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2015","unstructured":"Lammich, P.: Refinement to Imperative\/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 253\u2013269. Springer, Switzerland (2015)"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/978-3-642-14052-5_24","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2010","unstructured":"Lammich, P., Lochbihler, A.: The Isabelle collections framework. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 339\u2013354. Springer, Heidelberg (2010)"},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"Lammich, P., Neumann, R.: A Framework for Verifying Depth-First Search Algorithms. In: CPP, pp. 137\u2013146. ACM, 13 January 2015","DOI":"10.1145\/2676724.2693165"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 7406, pp. 166\u2013182. Springer, Heidelberg (2012)"},{"key":"23_CR18","unstructured":"Lochbihler, A.: Coinductive. Archive of Formal Proofs, February 2010. http:\/\/afp.sf.net\/entries\/Coinductive.shtml , formal proof development"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/3-540-17906-2_30","volume-title":"Advances in Petri Nets 1986. Proceedings of an Advanced Course, Bad Honnef, 8.-19. September 1986","author":"A Mazurkiewicz","year":"1987","unstructured":"Mazurkiewicz, A.: Trace theory. In: Reisig, W., Brauer, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 255, pp. 278\u2013324. Springer, Heidelberg (1987)"},{"key":"23_CR20","unstructured":"Merz, S.: Stuttering equivalence. Archive of Formal Proofs, May 2012. http:\/\/afp.sf.net\/entries\/Stuttering_Equivalence.shtml , formal proof development"},{"issue":"1","key":"23_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/jpdc.1996.0041","volume":"34","author":"M Naimi","year":"1996","unstructured":"Naimi, M., Trehel, M., Arnold, A.: A log (n) distributed mutual exclusion algorithm based on path reversal. J. Parallel Distrib. Comput. 34(1), 1\u201313 (1996)","journal-title":"J. Parallel Distrib. Comput."},{"key":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/978-3-319-12154-3_7","volume-title":"Verified Software: Theories, Tools and Experiments","author":"R Neumann","year":"2014","unstructured":"Neumann, R.: Using Promela in a fully verified executable LTL model checker. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 105\u2013114. Springer, Heidelberg (2014)"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"23_CR24","unstructured":"Paulson, L., Nipkow, T., Wenzel, M.: Isabelle (2014). http:\/\/isabelle.in.tum.de"},{"issue":"1","key":"23_CR25","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF00121262","volume":"8","author":"D Peled","year":"1996","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. Formal Meth. Syst. Des. 8(1), 39\u201364 (1996)","journal-title":"Formal Meth. Syst. Des."},{"issue":"5","key":"23_CR26","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/S0020-0190(97)00133-6","volume":"63","author":"D Peled","year":"1997","unstructured":"Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the next-time operator. Inf. Process. Lett. 63(5), 243\u2013246 (1997)","journal-title":"Inf. Process. Lett."},{"key":"23_CR27","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1017\/S0960129500001560","volume":"2","author":"P Wadler","year":"1992","unstructured":"Wadler, P.: Comprehending monads. Math. Struct. Comput. Sci. 2, 461\u2013493 (1992)","journal-title":"Math. Struct. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40648-0_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T03:11:20Z","timestamp":1567998680000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40648-0_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319406473","9783319406480"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40648-0_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}