Skip to main content
SpringerLink
Log in

Automated Verification of Relational While-Programs

  • Conference paper
Relational and Algebraic Methods in Computer Science (RAMICS 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8428))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Berghammer, R.: Combining relational calculus and the Dijkstra-Gries method for deriving relational programs. Information Sciences 119, 155–171 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  2. 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)

    Article  MATH  MathSciNet  Google Scholar 

  3. Berghammer, R., Hoffmann, T.: Relational depth-first-search with applications. Information Sciences 139, 167–186 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  4. Berghammer, R.: Applying relation algebra and Rel View to solve problems on orders and lattices. Acta Informatica 45, 211–236 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. 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)

    Google Scholar 

  7. Bibel, W., Schmitt, P.: Automated deduction: A basis for applications. Applied Logic Series. Kluwer (1998)

    Google Scholar 

  8. 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)

    MathSciNet  Google Scholar 

  9. 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)

    Google Scholar 

  10. Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM 18, 453–457 (1975)

    Article  MATH  MathSciNet  Google Scholar 

  11. Dijkstra, E.W.: A discipline of programming. Prentice-Hall (1976)

    Google Scholar 

  12. 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)

    Google Scholar 

  13. Gries, D.: The science of computer programming. Springer (1981)

    Google Scholar 

  14. 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)

    Google Scholar 

  15. 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)

    Chapter  Google Scholar 

  16. 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)

    Chapter  Google Scholar 

  17. 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)

    Google Scholar 

  18. Kahn, A.B.: Topological sorting of large networks. Communications of the ACM 5, 558–562 (1962)

    Article  MATH  Google Scholar 

  19. 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)

    Google Scholar 

  20. MacCaull, W., Orłowska, E.: Correspondence results for relational proof systems with application to the Lambek calculus. Studia Logica 71(3), 389–414 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  21. Müller-Olm, M., Seidl, H.: Computing polynomial program invariants. Information Processing Letters 91(5), 233–244 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  22. Schmidt, G., Ströhlein, T.: Relations and graphs, Discrete mathematics for computer scientists. EATCS Monographs on Theoretical Computer Science. Springer (1993)

    Google Scholar 

  23. Schmidt, G.: Relational mathematics. Encyclopedia of Mathematics and its Applications, vol. 132. Cambridge University Press (2010)

    Google Scholar 

  24. Schumann, J.: Automated theorem proving in software engineering. Springer (2001)

    Google Scholar 

  25. 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)

    Google Scholar 

  26. Tarski, A.: On the calculus of relations. Journal of Symbolic Logic 6(3), 73–89 (1941)

    Article  MathSciNet  Google Scholar 

  27. Tarski, A., Givant, S.: A formalization of set theory without variables, vol. 41. AMS Colloquium Publications (1987)

    Google Scholar 

  28. 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)

    Chapter  Google Scholar 

  29. 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)

    Chapter  Google Scholar 

  30. Rel View homepage: http://www.informatik.uni-kiel.de/~progsys/relview/ (accessed April 30, 2013)

  31. McCune, W.W.: Prover9 and Mace4., http://www.cs.unm.edu/~mccune/prover9 (accessed April 30, 2013)

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Christian-Albrechts-Universität zu Kiel, Germany

    Rudolf Berghammer & Insa Stucke

  2. NICTA, Australia

    Peter Höfner

  3. Computer Science and Engineering, University of New South Wales, Australia

    Peter Höfner

Authors
  1. Rudolf Berghammer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter Höfner
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Insa Stucke
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NICTA and UNSW, Anzac Parade 223, 2033, Kensington, NSW, Australia

    Peter Höfner

  2. School of Computational Sciences, Chapman University, One University Drive, 92866, Orange, CA, USA

    Peter Jipsen

  3. Department of Computing and Software, McMaster University, 1280 Main Street West, L8S 4K1, Hamilton, ON, Canada

    Wolfram Kahl

  4. Department of Computer Science, University of Augsburg, Universitätsstraße 6a, 86159, Augsburg, Germany

    Martin Eric Müller

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation