{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T20:50:38Z","timestamp":1725742238332},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642396335"},{"type":"electronic","value":"9783642396342"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39634-2_16","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T09:52:36Z","timestamp":1374486756000},"page":"197-212","source":"Crossref","is-referenced-by-count":10,"title":["Program Analysis and Verification Based on Kleene Algebra in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Alasdair","family":"Armstrong","sequence":"first","affiliation":[]},{"given":"Georg","family":"Struth","sequence":"additional","affiliation":[]},{"given":"Tjark","family":"Weber","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1-2","key":"16_CR1","doi-asserted-by":"publisher","first-page":"9","DOI":"10.3166\/jancl.16.9-33","volume":"16","author":"K. Aboul-Hosn","year":"2006","unstructured":"Aboul-Hosn, K., Kozen, D.: KAT-ML: An interactive theorem prover for Kleene algebra with tests. Journal of Applied Non-Classical Logics\u00a016(1-2), 9\u201334 (2006)","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"16_CR2","unstructured":"Angus, A., Kozen, D.: Kleene algebra with tests and program schematology. Technical Report TR2001-1844, Computer Science Department, Cornell University (July 2001)"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-33314-9_5","volume-title":"Relational and Algebraic Methods in Computer Science","author":"A. Armstrong","year":"2012","unstructured":"Armstrong, A., Struth, G.: Automated reasoning in higher-order regular algebra. In: Kahl, W., Griffin, T.G. (eds.) RAMICS 2012. LNCS, vol.\u00a07560, pp. 66\u201381. Springer, Heidelberg (2012)"},{"key":"16_CR4","unstructured":"Armstrong, A., Struth, G., Weber, T.: Kleene algebra. Archive of Formal Proofs, Formal proof development (2013), \n                    \n                      http:\/\/afp.sf.net\/entries\/Kleene_Algebra.shtml"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-13321-3_4","volume-title":"Mathematics of Program Construction","author":"R. Berghammer","year":"2010","unstructured":"Berghammer, R., Struth, G.: On automated program construction and verification. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol.\u00a06120, pp. 22\u201341. Springer, Heidelberg (2010)"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Braibant, T., Pous, D.: Deciding Kleene algebras in Coq. Logical Methods in Computer Science\u00a08(1) (2012)","DOI":"10.2168\/LMCS-8(1:16)2012"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/10722010_4","volume-title":"Mathematics of Program Construction","author":"E. Cohen","year":"2000","unstructured":"Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, pp. 45\u201359. Springer, Heidelberg (2000)"},{"key":"16_CR8","first-page":"101","volume-title":"Reflections on the Work of C. A. R. Hoare","author":"H. Collavizza","year":"2010","unstructured":"Collavizza, H., Gordon, M.: Forward with Hoare. In: Roscoe, A.W., Jones, C.B., Wood, K.R. (eds.) Reflections on the Work of C. A. R. Hoare, pp. 101\u2013121. Springer, Heidelberg (2010)"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Desharnais, J., M\u00f6ller, B., Struth, G.: Algebraic notions of termination. Logical Methods in Computer Science\u00a07(1) (2011)","DOI":"10.2168\/LMCS-7(1:1)2011"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-540-24771-5_10","volume-title":"Relational and Kleene-Algebraic Methods in Computer Science","author":"T. Ehm","year":"2004","unstructured":"Ehm, T., M\u00f6ller, B., Struth, G.: Kleene modules. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol.\u00a03051, pp. 112\u2013124. Springer, Heidelberg (2004)"},{"issue":"2","key":"16_CR11","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/j.scico.2006.01.009","volume":"65","author":"T. Fernandes","year":"2007","unstructured":"Fernandes, T., Desharnais, J.: Describing data flow analysis techniques with Kleene algebra. Sci. Comput. Program.\u00a065(2), 173\u2013194 (2007)","journal-title":"Sci. Comput. Program."},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-642-31365-3_22","volume-title":"Automated Reasoning","author":"S. Foster","year":"2012","unstructured":"Foster, S., Struth, G.: Automated analysis of regular algebra. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 271\u2013285. Springer, Heidelberg (2012)"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1007\/978-3-642-24559-6_41","volume-title":"Formal Methods and Software Engineering","author":"W. Guttmann","year":"2011","unstructured":"Guttmann, W., Struth, G., Weber, T.: Automating algebraic methods in Isabelle. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol.\u00a06991, pp. 617\u2013632. Springer, Heidelberg (2011)"},{"key":"16_CR14","unstructured":"Guttmann, W., Struth, G., Weber, T.: A repository for Tarski-Kleene algebras. In: H\u00f6fner, P., McIver, A., Struth, G. (eds.) ATE 2011. CEUR Workshop Proceedings, vol.\u00a0760, pp. 30\u201339. CEUR-WS.org (2011)"},{"key":"16_CR15","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-73595-3_19","volume-title":"Automated Deduction \u2013 CADE-21","author":"P. H\u00f6fner","year":"2007","unstructured":"H\u00f6fner, P., Struth, G.: Automated reasoning in Kleene algebra. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 279\u2013294. Springer, Heidelberg (2007)"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and Transfer: A modular design for quotients in Isabelle\/HOL. In: Isabelle Users Workshop (2012)","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, C.: Quotients revisited for Isabelle\/HOL. In: Chu, W.C., Wong, W.E., Palakal, M.J., Hung, C.-C. (eds.) SAC, pp. 1639\u20131644. ACM (2011)","DOI":"10.1145\/1982185.1982529"},{"issue":"3","key":"16_CR18","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D. Kozen","year":"1997","unstructured":"Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst.\u00a019(3), 427\u2013443 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR19","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/3-540-44957-4_38","volume-title":"Computational Logic - CL 2000","author":"D. Kozen","year":"2000","unstructured":"Kozen, D., Patron, M.-C.: Certification of compiler optimizations using Kleene algebra with tests. In: Palamidessi, C., et al. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 568\u2013582. Springer, Heidelberg (2000)"},{"issue":"2","key":"16_CR20","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/j.jlap.2005.04.004","volume":"66","author":"H. Lei\u00df","year":"2006","unstructured":"Lei\u00df, H.: Kleene modules and linear languages. J. Log. Algebr. Program.\u00a066(2), 185\u2013194 (2006)","journal-title":"J. Log. Algebr. Program."},{"key":"16_CR21","unstructured":"Manna, Z.: Mathematical theory of computation. McGraw-Hill (1974)"},{"issue":"2","key":"16_CR22","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/j.tcs.2005.09.069","volume":"351","author":"B. M\u00f6ller","year":"2006","unstructured":"M\u00f6ller, B., Struth, G.: Algebras of modal operators and partial correctness. Theor. Comput. Sci.\u00a0351(2), 221\u2013239 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: Dependent types for imperative programs. In: Hook, J., Thiemann, P. (eds.) ICFP, pp. 229\u2013240. ACM (2008)","DOI":"10.1145\/1411203.1411237"},{"issue":"2","key":"16_CR24","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s001650050009","volume":"10","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics. Formal Asp. Comput.\u00a010(2), 171\u2013186 (1998)","journal-title":"Formal Asp. Comput."},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"16_CR26","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of sequential imperative programs in Isabelle-HOL. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2006)","DOI":"10.1007\/978-3-540-32275-7_26"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39634-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:51:38Z","timestamp":1558302698000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39634-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396335","9783642396342"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}