{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:02:23Z","timestamp":1762459343307},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2016,4,1]],"date-time":"2016-04-01T00:00:00Z","timestamp":1459468800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We present a principled modular approach to the development of construction and verification tools for imperative programs, in which the control flow and the data flow are cleanly separated. Our simplest verification tool uses Kleene algebra with tests for the control flow of while-programs and their standard relational semantics for the data flow. It is expanded to a basic program construction tool by adding an operation for the specification statement and one single axiom. To include recursive procedures, Kleene algebras with tests are expanded further to quantales with tests. In this more expressive setting, iteration and the specification statement can be defined explicitly and stronger program transformation rules can be derived. Programming our approach in the Isabelle\/HOL interactive theorem prover yields simple lightweight mathematical components as well as program construction and verification tools that are correct by construction themselves. Verification condition generation and program construction rules are based on equational reasoning and supported by powerful Isabelle tactics and automated theorem proving. A number of examples shows our tools at work.<\/jats:p>","DOI":"10.1007\/s00165-015-0343-1","type":"journal-article","created":{"date-parts":[[2015,11,20]],"date-time":"2015-11-20T09:34:45Z","timestamp":1448012085000},"page":"265-293","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["Building program construction and verification tools from algebraic principles"],"prefix":"10.1145","volume":"28","author":[{"given":"Alasdair","family":"Armstrong","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Sheffield, Sheffield, UK"}]},{"given":"Victor B. F.","family":"Gomes","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Sheffield, Sheffield, UK"}]},{"given":"Georg","family":"Struth","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Sheffield, Sheffield, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Aarts CJ (1992) Galois connections presented calculationally"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Apt KR de Boer FS Olderog E-R (2009) Verification of sequential and concurrent programs. Springer","DOI":"10.1007\/978-1-84882-745-5"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Armstrong A Gomes VBF Struth G (2014) Algebraic principles for rely-guarantee style concurrency verification tools. In: Jones CB Pihlajasaari P Sun J (eds) FM 2014. LNCS vol 8442. Springer pp 78\u201393","DOI":"10.1007\/978-3-319-06410-9_6"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Armstrong A Gomes VBF Struth G (2014) Algebras for program correctness in Isabelle\/HOL. In: H\u00f6fner P et~al (eds) RAMiCS 2014.LNCS vol 8428. Springer pp 49\u201364","DOI":"10.1007\/978-3-319-06251-8_4"},{"key":"e_1_2_1_2_5_2","unstructured":"Armstrong A Gomes VBF Struth G (2014) Kleene algebras with tests and demonic refinement algebras. Archive of Formal Proofs"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Armstrong A Gomes VBF Struth G (2014) Lightweight program construction and verification tools in Isabelle\/HOL. In: Giannakopoulou D Sala\u00fcn G (eds) SEFM 2014 LNCS. Springer pp 5\u201319","DOI":"10.1007\/978-3-319-10431-7_2"},{"key":"e_1_2_1_2_7_2","unstructured":"Angus A Kozen D (2001) Kleene algebra with tests and program schematology. Technical Report TR2001-1844 Cornell University"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Armstrong A Struth G (2012) Automated reasoning in higher-order regular algebra. In: Griffin T Kahl W (eds) RAMiCs 2012. LNCS vol 7560. Springer","DOI":"10.1007\/978-3-642-33314-9_5"},{"key":"e_1_2_1_2_9_2","unstructured":"Armstrong A Struth G Weber T (2013) Kleene algebra. Archive of Formal Proofs"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Armstrong A Struth G Weber T (2013) Program analysis and verification based on Kleene algebra in Isabelle\/HOL. In: Blazy S Paulin-Mohring C Pichardie D (eds) ITP 2013. LNCS vol 7998. Springer pp 197\u2013212","DOI":"10.1007\/978-3-642-39634-2_16"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2014.02.001"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Bulwahn L Krauss A Haftmann F Erk\u00f6k L Matthews J (2008) Imperative functional programming with Isabelle\/HOL. In: A\u00eft Mohamed O Mu\u00f1oz CA Tahar S (eds) TPHOLs 2008. LNCS vol 5170. Springer pp 134\u2013149","DOI":"10.1007\/978-3-540-71067-7_14"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Braibant T Pous D (2010) An efficient Coq tactic for deciding Kleene algebras. In K. Kaufmann and L. C. Paulson editors ITP 2010 volume 6172 of LNCS pages 163\u2013178. Springer","DOI":"10.1007\/978-3-642-14052-5_13"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0006-5"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Dongol B Gomes VBF Struth G (2015) A program construction and verification tool for separation logic. In: Hinze R Voigtl\u00e4nder J (eds) MPC 2015. LNCS vol 9129. Springer pp 137\u2013158","DOI":"10.1007\/978-3-319-19797-5_7"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.05.007"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre J-C Paskevich A (2013) Why3\u2014where programs meet provers. In: Felleisen M Gardner P (eds) ESOP 201. LNCS vol 7792. Springer pp 125\u2013128","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Haftmann F Krauss A Kuncar O Nipkow T (2013) Data refinement in Isabelle\/HOL. In: Blazy S Paulin-Mohring C Pichardie D (eds) ITP 2013. LNCS vol 7998. Springer pp 100\u2013115","DOI":"10.1007\/978-3-642-39634-2_10"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"H\u00f6fner P Struth G (2007) Automated reasoning in Kleene algebra. In: Pfenning F (ed) CADE-21. LNCS vol 4603. Springer pp 279\u2013294","DOI":"10.1007\/978-3-540-73595-3_19"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050057"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9223-4"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"issue":"1","key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1145\/343369.343378","article-title":"On Hoare logic and Kleene algebra with tests","volume":"1","author":"Kozen D","year":"2000","journal-title":"ACM TOCL"},{"key":"e_1_2_1_2_24_2","unstructured":"Kozen D (2003) Kleene algebras with tests and the static analysis of programs. Technical Report TR2003-1915 Cornell University"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Kozen D Patron M-C (2000) Certification of compiler optimizations using Kleene algebra with tests. In: Lloyd JW et\u00a0al (eds) CL 2000. LNAI vol 1861. Springer pp 568\u2013582","DOI":"10.1007\/3-540-44957-4_38"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Kozen D Smith F (1997) Kleene algebra with tests: completeness and decidability. In: van Dalen D Bezem M (eds) CSL\u201996. LNCS vol 1258. Springer pp 244\u2013259","DOI":"10.1007\/3-540-63172-0_43"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Leino RKM (2010) Dafny: an automatic program verifier for functional correctness. In: Clarke EMC Voronkov A (eds) LPAR-16 LNCS vol 6355. Springer pp 348\u2013370","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Meijer E Fokkinga M Paterson R (1991) Functional programming with bananas lenses envelopes and barbed wire. In: Hughes J (ed) 5th ACM Conf. Functional Programming Languages and Computer Architecture. LNCS vol 523. Springer pp 124\u2013144","DOI":"10.1007\/3540543961_7"},{"key":"e_1_2_1_2_29_2","unstructured":"Morgan C (1994) Programming from specifications 2nd edn. Prentice Hall"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.09.069"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"M\u00f6ller B Struth G (2006) wp is wlp. In: MacCaull W Winter M D\u00fcntsch I (eds) RelMiCS 2005. LNCS vol 3929. Springer pp 200\u2013211","DOI":"10.1007\/11734673_16"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050009"},{"key":"#cr-split#-e_1_2_1_2_33_2.1","doi-asserted-by":"crossref","unstructured":"Nipkow T (2002) Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield JC","DOI":"10.1007\/3-540-45793-3_8"},{"key":"#cr-split#-e_1_2_1_2_33_2.2","doi-asserted-by":"crossref","unstructured":"(ed) CSL 2002. LNCS vol 2471. Springer pp 103-119","DOI":"10.3917\/cjung.103.0119"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Nipkow T Paulson LC Wenzel M (2002) Isabelle\/HOL\u2014a proof assistant for higher-order logic. LNCS vol 2283. Springer","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Pous D (2013) Kleene algebra with tests and Coq tools for while programs. In: Blazy S Paulin-Mohring C Pichardie D (eds) ITP. LNCS vol 7998. Springer pp 180\u2013196","DOI":"10.1007\/978-3-642-39634-2_15"},{"key":"e_1_2_1_2_37_2","unstructured":"Schirmer N (2008) A sequential imperative programming language syntax semantics Hoare logics and verification environment. Archive of Formal Proofs"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Sternagel C Thiemann R (2012) Certification of nontermination proofs. In: Beringer L Felty AP (eds) ITP 2012. LNCS vol 7406. Springer pp 266\u2013282","DOI":"10.1007\/978-3-642-32347-8_18"},{"key":"e_1_2_1_2_39_2","unstructured":"Stoy JE (1977) Denotational semantics: the scott-strachey approach to programming language theory. MIT Press"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.09.065"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-015-0343-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-015-0343-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-015-0343-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:55:21Z","timestamp":1641538521000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-015-0343-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,4]]}},"alternative-id":["10.1007\/s00165-015-0343-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-015-0343-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,4]]}}}