Abstract
Software verification is essential for safety-critical systems. In this paper, we illustrate that some verification tasks can be done fully automatically. We show how to automatically verify imperative programs for relation-based discrete structures by combining relation algebra and the well-known assertion-based verification method with automated theorem proving. We present two examples in detail: a relational program for determining the reflexive-transitive closure and a topological sorting algorithm. We also treat the automatic verification of the equivalence of common-logical and relation-algebraic specifications.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Berghammer, R.: Combining relational calculus and the Dijkstra-Gries method for deriving relational programs. Information Sciences 119, 155–171 (1999)
Berghammer, R., Hoffmann, T.: Deriving relational programs for computing kernels by reconstructing a proof of Richardson’s theorem. Science of Computer Programming 38, 1–25 (2000)
Berghammer, R., Hoffmann, T.: Relational depth-first-search with applications. Information Sciences 139, 167–186 (2001)
Berghammer, R.: Applying relation algebra and Rel View to solve problems on orders and lattices. Acta Informatica 45, 211–236 (2008)
Berghammer, R., Struth, G.: On automated program construction and verification. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol. 6120, pp. 22–41. Springer, Heidelberg (2010)
Berghammer, R., Fischer, S.: Simple rectangle-based functional programs for computing reflexive-transitive closures. In: Kahl, W., Griffin, T.G. (eds.) RAMiCS 2012. LNCS, vol. 7560, pp. 114–129. Springer, Heidelberg (2012)
Bibel, W., Schmitt, P.: Automated deduction: A basis for applications. Applied Logic Series. Kluwer (1998)
Chin, L.H., Tarski, A.: Distributive and modular laws in the arithmetic of relation algebras. Univ. of California Publ. Math. (new series) 1, 341–384 (1951)
Dang, H.H., Höfner, P.: First-order theorem prover evaluation w.r.t. relation- and Kleene algebra. In: Berghammer, R., Möller, B., Struth, G. (eds.) Relations and Kleene Algebra in Computer Science – Ph.D. Programme at RelMiCS 10/AKA 05. Technical Report 2008-04, Institut für Informatik, Universität Augsburg, 48-52 (2008)
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM 18, 453–457 (1975)
Dijkstra, E.W.: A discipline of programming. Prentice-Hall (1976)
Foster, S., Struth, G., Weber, T.: Automated engineering of relational and algebraic methods in Isabelle/HOL (invited Tutorial). In: de Swart, H. (ed.) RAMiCS 2011. LNCS, vol. 6663, pp. 52–67. Springer, Heidelberg (2011)
Gries, D.: The science of computer programming. Springer (1981)
Hattensperger, C., Berghammer, R., Schmidt, G.: RALF – A relation-algebraic formula manipulation system and proof checker. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds.) Algebraic Methodology and Software Technology. Workshops in Computing, pp. 407–408. Springer (1993)
Höfner, P., Struth, G.: Automated reasoning in Kleene Algebra. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 279–294. Springer, Heidelberg (2007)
Höfner, P., Struth, G.: On automating the calculus of relations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 50–66. Springer, Heidelberg (2008)
Kahl, W.: Calculational relation-algebraic proofs in Isabelle/Isar. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS/Kleene-Algebra Ws 2003. LNCS, vol. 3051, pp. 178–190. Springer, Heidelberg (2004)
Kahn, A.B.: Topological sorting of large networks. Communications of the ACM 5, 558–562 (1962)
Kovács, L.: Invariant generation for P-solvable loops with assignments. In: Hirsch, E.A., Razborov, A.A., Semenov, A., Slissenko, A. (eds.) CSR 2008. LNCS, vol. 5010, pp. 349–359. Springer, Heidelberg (2008)
MacCaull, W., Orłowska, E.: Correspondence results for relational proof systems with application to the Lambek calculus. Studia Logica 71(3), 389–414 (2002)
Müller-Olm, M., Seidl, H.: Computing polynomial program invariants. Information Processing Letters 91(5), 233–244 (2004)
Schmidt, G., Ströhlein, T.: Relations and graphs, Discrete mathematics for computer scientists. EATCS Monographs on Theoretical Computer Science. Springer (1993)
Schmidt, G.: Relational mathematics. Encyclopedia of Mathematics and its Applications, vol. 132. Cambridge University Press (2010)
Schumann, J.: Automated theorem proving in software engineering. Springer (2001)
Sinz, C.: System description: ARA – An automated theorem prover for relation algebras. In: McAllester, D. (ed.) CADE-17. LNCS (LNAI), vol. 1831, pp. 177–182. Springer, Heidelberg (2000)
Tarski, A.: On the calculus of relations. Journal of Symbolic Logic 6(3), 73–89 (1941)
Tarski, A., Givant, S.: A formalization of set theory without variables, vol. 41. AMS Colloquium Publications (1987)
von Oheimb, D., Gritzner, T.F.: RALL: Machine-supported proofs for relation algebra. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol. 1249, pp. 380–394. Springer, Heidelberg (1997)
Weidenbach, C., Schmidt, R.A., Hillenbrand, T., Rusev, R., Topic, D.: System description: SPASS version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 514–520. Springer, Heidelberg (2007)
Rel View homepage: http://www.informatik.uni-kiel.de/~progsys/relview/ (accessed April 30, 2013)
McCune, W.W.: Prover9 and Mace4., http://www.cs.unm.edu/~mccune/prover9 (accessed April 30, 2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Berghammer, R., Höfner, P., Stucke, I. (2014). Automated Verification of Relational While-Programs. In: Höfner, P., Jipsen, P., Kahl, W., Müller, M.E. (eds) Relational and Algebraic Methods in Computer Science. RAMICS 2014. Lecture Notes in Computer Science, vol 8428. Springer, Cham. https://doi.org/10.1007/978-3-319-06251-8_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-06251-8_11
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06250-1
Online ISBN: 978-3-319-06251-8
eBook Packages: Computer ScienceComputer Science (R0)