{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T12:26:15Z","timestamp":1725798375801},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319104300"},{"type":"electronic","value":"9783319104317"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10431-7_2","type":"book-chapter","created":{"date-parts":[[2014,8,4]],"date-time":"2014-08-04T09:27:28Z","timestamp":1407144448000},"page":"5-19","source":"Crossref","is-referenced-by-count":2,"title":["Lightweight Program Construction and Verification Tools in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Alasdair","family":"Armstrong","sequence":"first","affiliation":[]},{"given":"Victor B. F.","family":"Gomes","sequence":"additional","affiliation":[]},{"given":"Georg","family":"Struth","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"Angus, A., Kozen, D.: Kleene algebra with tests and program schematology. Technical Report TR2001-1844, Cornell University (2001)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-319-06410-9_6","volume-title":"FM 2014: Formal Methods","author":"A. Armstrong","year":"2014","unstructured":"Armstrong, A., Gomes, V.B.F., Struth, G.: Algebraic principles for rely-guarantee style concurrency verification tools. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol.\u00a08442, pp. 78\u201393. Springer, Heidelberg (2014)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-06251-8_4","volume-title":"Relational and Algebraic Methods in Computer Science","author":"A. Armstrong","year":"2014","unstructured":"Armstrong, A., Gomes, V.B.F., Struth, G.: Algebras for program correctness in Isabelle\/HOL. In: H\u00f6fner, P., Jipsen, P., Kahl, W., M\u00fcller, M.E. (eds.) RAMiCS 2014. LNCS, vol.\u00a08428, pp. 49\u201364. Springer, Heidelberg (2014)"},{"key":"2_CR4","unstructured":"Armstrong, A., Gomes, V.B.F., Struth, G.: Kleene algebras with tests and demonic refinement algebras. Archive of Formal Proofs (2014)"},{"key":"2_CR5","unstructured":"Armstrong, A., Struth, G., Weber, T.: Kleene algebra. Archive of Formal Proofs (2013)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-39634-2_16","volume-title":"Interactive Theorem Proving","author":"A. Armstrong","year":"2013","unstructured":"Armstrong, A., Struth, G., Weber, T.: Program analysis and verification based on Kleene algebra in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 197\u2013212. Springer, Heidelberg (2013)"},{"issue":"2-3","key":"2_CR7","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/s00165-003-0006-5","volume":"15","author":"A. Cavalcanti","year":"2003","unstructured":"Cavalcanti, A., Sampaio, A., Woodcock, J.: A refinement strategy for circus. Formal Aspects of Computing\u00a015(2-3), 146\u2013181 (2003)","journal-title":"Formal Aspects of Computing"},{"issue":"3","key":"2_CR8","doi-asserted-by":"publisher","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. Science of Computer Programming\u00a076(3), 181\u2013203 (2011)","journal-title":"Science of Computer Programming"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 173\u2013177. Springer, Heidelberg (2007)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-39634-2_10","volume-title":"Interactive Theorem Proving","author":"F. Haftmann","year":"2013","unstructured":"Haftmann, F., Krauss, A., Kun\u010dar, O., Nipkow, T.: Data refinement in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 100\u2013115. Springer, Heidelberg (2013)"},{"issue":"3","key":"2_CR11","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 TOPLAS\u00a019(3), 427\u2013443 (1997)","journal-title":"ACM TOPLAS"},{"issue":"1","key":"2_CR12","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/343369.343378","volume":"1","author":"D. Kozen","year":"2000","unstructured":"Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM TOCL\u00a01(1), 60\u201376 (2000)","journal-title":"ACM TOCL"},{"key":"2_CR13","unstructured":"Kozen, D.: Kleene algebras with tests and the static analysis of programs. Technical Report TR2003-1915, Cornell University (2003)"},{"key":"2_CR14","series-title":"Lecture Notes in Artificial Intelligence","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: Lloyd, J., et al. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 568\u2013582. Springer, Heidelberg (2000)"},{"issue":"2","key":"2_CR15","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. Theoretical Computer Science\u00a0351(2), 221\u2013239 (2006)","journal-title":"Theoretical Computer Science"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/11734673_16","volume-title":"Relational Methods in Computer Science","author":"B. M\u00f6ller","year":"2006","unstructured":"M\u00f6ller, B., Struth, G.: wp is wlp. In: MacCaull, W., Winter, M., D\u00fcntsch, I. (eds.) RelMiCS 2005. LNCS, vol.\u00a03929, pp. 200\u2013211. Springer, Heidelberg (2006)"},{"key":"2_CR17","unstructured":"Morgan, C.: Programming from specifications, 2nd edn. Prentice Hall (1994)"},{"key":"2_CR18","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., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"2","key":"2_CR19","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 Aspects of Computing\u00a010(2), 171\u2013186 (1998)","journal-title":"Formal Aspects of Computing"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-642-39634-2_15","volume-title":"Interactive Theorem Proving","author":"D. Pous","year":"2013","unstructured":"Pous, D.: Kleene algebra with tests and Coq tools for while programs. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 180\u2013196. Springer, Heidelberg (2013)"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-642-32347-8_18","volume-title":"Interactive Theorem Proving","author":"C. Sternagel","year":"2012","unstructured":"Sternagel, C., Thiemann, R.: Certification of nontermination proofs. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 266\u2013282. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10431-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,31]],"date-time":"2019-01-31T04:26:00Z","timestamp":1548908760000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10431-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319104300","9783319104317"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10431-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}