zbMATH — the first resource for mathematics

Building program construction and verification tools from algebraic principles. (English) Zbl 1342.68066
Summary: 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.
Reviewer: Reviewer (Berlin)

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] Aarts CJ (1992) Galois connections presented calculationally · Zbl 1269.68090
[2] Apt KR, de Boer FS, Olderog E-R (2009) Verification of sequential and concurrent programs. Springer · Zbl 1183.68361
[3] 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-93 · Zbl 1211.68242
[4] Armstrong A, Gomes VBF, Struth G (2014) Algebras for program correctness in Isabelle/HOL. In: Höfner P et al (eds) RAMiCS 2014.LNCS, vol 8428. Springer, pp 49-64 · Zbl 1405.68314
[5] Armstrong A, Gomes VBF, Struth G (2014) Kleene algebras with tests and demonic refinement algebras. Archive of Formal Proofs · Zbl 1093.68555
[6] Armstrong A, Gomes VBF, Struth G (2014) Lightweight program construction and verification tools in Isabelle/HOL. In: Giannakopoulou D, Salaün G (eds) SEFM 2014, LNCS. Springer, pp 5-19 · Zbl 1365.68326
[7] Angus A, Kozen D (2001) Kleene algebra with tests and program schematology. Technical Report TR2001-1844, Cornell University · Zbl 1434.68637
[8] Armstrong A, Struth G (2012) Automated reasoning in higher-order regular algebra. In: Griffin T, Kahl W (eds) RAMiCs 2012. LNCS, vol 7560. Springer · Zbl 1364.68326
[9] Armstrong A, Struth G, Weber T (2013) Kleene algebra. Archive of Formal Proofs · Zbl 0910.68138
[10] 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-212 · Zbl 1317.68201
[11] Armstrong, A; Struth, G; Weber, T, Programming and automating mathematics in the Tarski-Kleene hierarchy, J Log Algebr Methods Programm, 83, 87-102, (2014) · Zbl 1434.68637
[12] Bulwahn L, Krauss A, Haftmann F, Erkök L, Matthews J (2008) Imperative functional programming with Isabelle/HOL. In: Aït Mohamed O, Muñoz CA, Tahar S (eds) TPHOLs 2008. LNCS, vol 5170. Springer, pp 134-149 · Zbl 1165.68352
[13] 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-178. Springer · Zbl 1291.68330
[14] Cavalcanti, A; Sampaio, A; Woodcock, J, A refinement strategy for circus, Formal Aspects Comput, 15, 146-181, (2003) · Zbl 1093.68555
[15] Dongol B, Gomes VBF, Struth G (2015) A program construction and verification tool for separation logic. In: Hinze R, Voigtländer J (eds) MPC 2015. LNCS, vol 9129. Springer, pp 137-158 · Zbl 1432.68071
[16] Desharnais, J; Struth, G, Internal axioms for domain semirings, Sci Comput Program, 76, 181-203, (2011) · Zbl 1211.68242
[17] Filliâtre J-C, Paskevich A (2013) Why3—where programs meet provers. In: Felleisen M, Gardner P (eds) ESOP 201. LNCS, vol 7792. Springer, pp 125-128
[18] 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-115 · Zbl 1317.68212
[19] Höfner P, Struth G (2007) Automated reasoning in Kleene algebra. In: Pfenning F (ed) CADE-21. LNCS, vol 4603. Springer, pp 279-294 · Zbl 1184.68462
[20] Kleymann, T, Hoare logic and auxiliary variables, Formal Aspect Comput, 11, 541-566, (1999) · Zbl 0978.03026
[21] Krauss, A; Nipkow, T, Proof pearl: regular expression equivalence and relation algebra, J Autom Reason, 49, 95-106, (2012) · Zbl 1269.68090
[22] Kozen, D, Kleene algebra with tests, ACM TOPLAS, 19, 427-443, (1997) · Zbl 0882.03064
[23] Kozen, D, On Hoare logic and Kleene algebra with tests, ACM TOCL, 1, 60-76, (2000) · Zbl 1365.68326
[24] Kozen D (2003) Kleene algebras with tests and the static analysis of programs. Technical Report TR2003-1915, Cornell University
[25] Kozen D, Patron M-C (2000) Certification of compiler optimizations using Kleene algebra with tests. In: Lloyd JW et al (eds) CL 2000. LNAI, vol 1861. Springer, pp 568-582 · Zbl 0983.68032
[26] Kozen D, Smith F (1997) Kleene algebra with tests: completeness and decidability. In: van Dalen D, Bezem M (eds) CSL’96. LNCS, vol 1258. Springer, pp 244-259 · Zbl 0882.03064
[27] 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-370 · Zbl 1253.68095
[28] 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-144 · Zbl 1365.68326
[29] Morgan C (1994) Programming from specifications, 2nd edn. Prentice Hall · Zbl 0829.68083
[30] Möller, B; Struth, G, Algebras of modal operators and partial correctness, Theor Comput Sci, 351, 221-239, (2006) · Zbl 1086.68082
[31] Möller B, Struth G (2006) wp is wlp. In: MacCaull W, Winter M, Düntsch I (eds) RelMiCS 2005. LNCS, vol 3929. Springer, pp 200-211 · Zbl 1185.68227
[32] Nipkow, T, Winskel is (almost) right: towards a mechanized semantics, Formal Aspects Comput, 10, 171-186, (1998) · Zbl 0910.68138
[33] Nipkow T (2002) Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield JC (ed) CSL 2002. LNCS, vol 2471. Springer, pp 103-119 · Zbl 1020.03029
[34] Nanevski, A; Morrisett, JG; Birkedal, L, Hoare type theory, polymorphism and separation, J Funct Program, 18, 865-911, (2008) · Zbl 1155.68354
[35] Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL—a proof assistant for higher-order logic. LNCS, vol 2283. Springer
[36] 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-196 · Zbl 1317.68229
[37] Schirmer N (2008) A sequential imperative programming language syntax, semantics, Hoare logics and verification environment. Archive of Formal Proofs · Zbl 0910.68138
[38] Sternagel C, Thiemann R (2012) Certification of nontermination proofs. In: Beringer L, Felty AP (eds) ITP 2012. LNCS, vol 7406. Springer, pp 266-282 · Zbl 1360.68767
[39] Stoy JE (1977) Denotational semantics: the scott-strachey approach to programming language theory. MIT Press · Zbl 1155.68354
[40] Schirmer, N; Wenzel, M, State spaces—the locale way, ENTCS, 254, 161-179, (2009)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.