Skip to main content
SpringerLink
Log in
Book cover

International Conference on Relational and Algebraic Methods in Computer Science

RAMICS 2014: Relational and Algebraic Methods in Computer Science pp 49–64Cite as

Algebras for Program Correctness in Isabelle/HOL

  • Conference paper

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

Abstract

We present a reference formalisation of Kleene algebra and demonic refinement algebra with tests in Isabelle/HOL. It provides three different formalisations of tests. Our structured comprehensive libraries for these algebras extend an existing Kleene algebra library. It includes an algebraic account of Hoare logic for partial correctness and several refinement and concurrency control laws in a total correctness setting. Formalisation examples include a complex refinement theorem, a generic proof of a loop transformation theorem for partial and total correctness and a simple prototypical verification tool for while programs, which is itself formally verified.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Angus, A., Kozen, D.: Kleene algebra with tests and program schematology. Technical Report TR2001-1844, Computer Science Department, Cornell University (July 2001)

    Google Scholar 

  2. Armstrong, A., Gomes, V.B.F., Struth, G.: Algebraic principles for rely-guarantee style concurrency verification tools. CoRR, abs/1312.1225 (2013)

    Google Scholar 

  3. Armstrong, A., Gomes, V.B.F., Struth, G.: Kleene algebras with tests and demonic refinement algebras. Archive of Formal Proofs (2014)

    Google Scholar 

  4. Armstrong, A., Struth, G., Weber, T.: Kleene algebra. Archive of Formal Proofs (2013)

    Google Scholar 

  5. 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. 7998, pp. 197–212. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  6. Back, R.-J.R.: A method for refining atomicity in parallel algorithms. In: Odijk, E., Rem, M., Syre, J.-C. (eds.) PARLE 1989. LNCS, vol. 366, pp. 199–216. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

  7. Back, R.-J., Kurki-Suonio, R.: Distributed cooperation with action systems. ACM TOPLAS 10(4), 513–554 (1988)

    Article  MATH  Google Scholar 

  8. Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer (1998)

    Google Scholar 

  9. Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 45–59. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  10. Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall (1971)

    Google Scholar 

  11. Desharnais, J., Struth, G.: Internal axioms for domain semirings. Science of Computer Programming 76(3), 181–203 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  12. Foster, S., Struth, G.: Automated analysis of regular algebra. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 271–285. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  13. Höfner, P., Struth, G., Sutcliffe, G.: Automated verification of refinement laws. Ann. Mathematics and Artificial Intelligence 55(1-2), 35–62 (2009)

    Article  MATH  Google Scholar 

  14. Jónsson, B., Tarski, A.: Boolean algebras with operators, part 1. American Journal of Mathematics 73(4), 891–939 (1951)

    Article  MATH  MathSciNet  Google Scholar 

  15. Kozen, D.: Kleene algebra with tests. ACM TOPLAS 19(3), 427–443 (1997)

    Article  Google Scholar 

  16. Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM TOCL 1(1), 60–76 (2000)

    Article  MathSciNet  Google Scholar 

  17. Manes, E.G., Benson, D.B.: The inverse semigroup of a sum-ordered semiring. Semigroup Forum 31(1), 129–152 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  18. Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)

    Google Scholar 

  19. Preoteasa, V.: Algebra of monotonic boolean transformers. In: Simao, A., Morgan, C. (eds.) SBMF 2011. LNCS, vol. 7021, pp. 140–155. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  20. Rabehaja, T.M., Sanders, J.W.: Refinement algebra with explicit probabilism. In: Chin, W.-N., Qin, S. (eds.) TASE, pp. 63–70. IEEE Comp. Soc. (2009)

    Google Scholar 

  21. Solin, K.: Normal forms in total correctness for while programs and action systems. J. Logic and Algebraic Programming 80(6), 362–375 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  22. von Wright, J.: From Kleene algebra to refinement algebra. In: Boiten, E.A., Möller, B. (eds.) MPC 2002. LNCS, vol. 2386, pp. 233–262. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  23. von Wright, J.: Towards a refinement algebra. Science of Computer Programming 51(1-2), 23–45 (2004)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Sheffield, UK

    Alasdair Armstrong, Victor B. F. Gomes & Georg Struth

Authors
  1. Alasdair Armstrong
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Victor B. F. Gomes
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Georg Struth
    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

Armstrong, A., Gomes, V.B.F., Struth, G. (2014). Algebras for Program Correctness in Isabelle/HOL. 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_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-06251-8_4

  • 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