{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:03:51Z","timestamp":1762459431603,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319489889"},{"type":"electronic","value":"9783319489896"}],"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-48989-6_19","type":"book-chapter","created":{"date-parts":[[2016,11,7]],"date-time":"2016-11-07T06:31:19Z","timestamp":1478500279000},"page":"310-325","source":"Crossref","is-referenced-by-count":13,"title":["Modal Kleene Algebra Applied to Program Correctness"],"prefix":"10.1007","author":[{"given":"Victor B. F.","family":"Gomes","sequence":"first","affiliation":[]},{"given":"Georg","family":"Struth","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,11,8]]},"reference":[{"key":"19_CR1","unstructured":"Armstrong, A., Gomes, V.B.F., Struth, G.: Kleene algebra with tests and demonic refinement algebras. In: Archive of Formal Proofs (2014)"},{"issue":"2","key":"19_CR2","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/s00165-015-0343-1","volume":"28","author":"A Armstrong","year":"2016","unstructured":"Armstrong, A., Gomes, V.B.F., Struth, G.: Building program construction and verification tools from algebraic principles. Form. Asp. Comput. 28(2), 265\u2013293 (2016)","journal-title":"Form. Asp. Comput."},{"key":"19_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. 7560, pp. 66\u201381. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33314-9_5"},{"key":"19_CR4","unstructured":"Armstrong, A., Struth, G., Weber, T.: Kleene algebra. In: Archive of Formal Proofs (2013)"},{"issue":"2","key":"19_CR5","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/j.jlap.2014.02.001","volume":"83","author":"A Armstrong","year":"2014","unstructured":"Armstrong, A., Struth, G., Weber, T.: Programming, automating mathematics in the Tarski-Kleene hierarchy. J. Log. Algebraic Methods Program. 83(2), 87\u2013102 (2014)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"19_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus - A Systematic Introduction","author":"R Back","year":"1998","unstructured":"Back, R., von Wright, J.: Refinement Calculus - A Systematic Introduction. Springer, New York (1998)"},{"key":"19_CR7","volume-title":"Regular Algebra and Finite Machines","author":"JH Conway","year":"1971","unstructured":"Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall, London (1971)"},{"issue":"1","key":"19_CR8","first-page":"1","volume":"7","author":"J Desharnais","year":"2011","unstructured":"Desharnais, J., M\u00f6ller, B., Struth, G.: Algebraic notions of termination. Log. Methods Comput. Sci. 7(1), 1\u201329 (2011)","journal-title":"Log. Methods Comput. Sci."},{"issue":"3","key":"19_CR9","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/j.scico.2010.05.007","volume":"76","author":"J Desharnais","year":"2011","unstructured":"Desharnais, J., Struth, G.: Internal axioms for domain semirings. Sci. Comput. Program. 76(3), 181\u2013203 (2011)","journal-title":"Sci. Comput. Program."},{"key":"19_CR10","unstructured":"Gomes, V.B.F.: Algebraic principles for program correctness tools in Isabelle\/HOL. PhD thesis, University of Sheffield (2015)"},{"key":"19_CR11","unstructured":"Gomes, V.B.F., Guttman, W., H\u00f6fner, P., Struth, G., Weber, T.: Kleene algebra with domain. In: Archive of Formal Proofs (2016)"},{"key":"19_CR12","unstructured":"Gomes, V.B.F., Struth, G.: Program construction and verification components based on Kleene algebra. In: Archive of Formal Proofs (2016)"},{"key":"19_CR13","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-1-84882-912-1_5","volume-title":"Reflections on the Work of C.A.R. Hoare","author":"M Gordon","year":"2010","unstructured":"Gordon, M., Collavizza, H.: Forward with Hoare. In: Roscoe, A.W., Jones, C.B., Wood, K.W. (eds.) Reflections on the Work of C.A.R. Hoare, pp. 101\u2013121. Springer, London (2010). doi: 10.1007\/978-1-84882-912-1_5"},{"key":"19_CR14","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"issue":"4","key":"19_CR15","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1023\/A:1008271805106","volume":"6","author":"M Hollenberg","year":"1997","unstructured":"Hollenberg, M.: An equational axiomatization of dynamic negation and relational composition. J. Log. Lang. Inf. 6(4), 381\u2013401 (1997)","journal-title":"J. Log. Lang. Inf."},{"issue":"4","key":"19_CR16","doi-asserted-by":"crossref","first-page":"207","DOI":"10.2307\/2372123","volume":"73","author":"B J\u00f3nsson","year":"1951","unstructured":"J\u00f3nsson, B., Tarski, A.: Boolean algebras with operators, Part I. Am. J. Math. 73(4), 207\u2013215 (1951)","journal-title":"Am. J. Math."},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/3-540-44957-4_38","volume-title":"Computational Logic \u2014 CL 2000","author":"D Kozen","year":"2000","unstructured":"Kozen, D., Patron, M.-C.: Certification of compiler optimizations using Kleene algebra with tests. In: Lloyd, J., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Palamidessi, C., Pereira, L.M., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 568\u2013582. Springer, Heidelberg (2000). doi: 10.1007\/3-540-44957-4_38"},{"issue":"3","key":"19_CR18","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/s10817-015-9360-2","volume":"56","author":"D Matichuk","year":"2016","unstructured":"Matichuk, D., Murray, T.C., Wenzel, M.: Eisbach: a proof method language for Isabelle. J. Autom. Reason. 56(3), 261\u2013282 (2016)","journal-title":"J. Autom. Reason."},{"key":"19_CR19","unstructured":"Meng, J., Paulson, L.C., Klein, G.: A termination checker for Isabelle Hoare logic. In: International Verification Workshop (2007)"},{"issue":"2","key":"19_CR20","doi-asserted-by":"crossref","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. 351(2), 221\u2013239 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"19_CR21","volume-title":"Programming from Specifications","author":"C Morgan","year":"1994","unstructured":"Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall, London (1994)","edition":"2"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/3-540-10854-8_31","volume-title":"Fundamentals of Computation Theory","author":"I N\u00e9meti","year":"1981","unstructured":"N\u00e9meti, I.: Dynamic algebras of programs. In: Gecseg, F. (ed.) FCT 1981. LNCS, vol. 117, pp. 281\u2013290. Springer, Heidelberg (1981)"},{"key":"19_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics-With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics-With Isabelle\/HOL. Springer, Switzerland (2014)"},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-31623-4_3","volume-title":"Descriptional Complexity of Formal Systems","author":"A Platzer","year":"2012","unstructured":"Platzer, A.: Logical analysis of hybrid systems. In: Kutrib, M., Moreira, N., Reis, R. (eds.) DCFS 2012. LNCS, vol. 7386, pp. 43\u201349. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31623-4_3"},{"key":"19_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BFb0043079","volume-title":"Algebraic Logic and Universal Algebra in Computer Science","author":"V Pratt","year":"1990","unstructured":"Pratt, V.: Dynamic algebras as a well-behaved fragment of relation algebras. In: Bergman, C.H., Maddux, R.D., Pigozzi, D.L. (eds.) Algebraic Logic and Universal Algebra in Computer Science. LNCS, vol. 425, pp. 77\u2013110. Springer, Heidelberg (1990). doi: 10.1007\/BFb0043079"},{"issue":"6","key":"19_CR27","doi-asserted-by":"crossref","first-page":"705","DOI":"10.1016\/j.jlap.2012.05.004","volume":"81","author":"G Struth","year":"2012","unstructured":"Struth, G.: Left omega algebras and regular equations. J. Log. Algebraic Program. 81(6), 705\u2013717 (2012)","journal-title":"J. Log. Algebraic Program."},{"issue":"4","key":"19_CR28","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1016\/j.ipl.2015.11.007","volume":"116","author":"G Struth","year":"2016","unstructured":"Struth, G.: On the expressive power of Kleene algebra with domain. Inf. Proces. Lett. 116(4), 284\u2013288 (2016)","journal-title":"Inf. Proces. Lett."}],"container-title":["Lecture Notes in Computer Science","FM 2016: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48989-6_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T11:28:26Z","timestamp":1718882906000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48989-6_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319489889","9783319489896"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48989-6_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}