Skip to main content
SpringerLink
Log in
Book cover

International Conference on Integrated Formal Methods

IFM 2004: Integrated Formal Methods pp 207–226Cite as

Software Verification with Integrated Data Type Refinement for Integer Arithmetic

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2999))

Abstract

We present an approach to integrating the refinement relation between infinite integer types (used in specification languages) and finite integer types (used in programming languages) into software verification calculi. Since integer types in programming languages have finite ranges, in general they are not a correct data refinement of the mathematical integers usually used in specification languages. Ensuring the correctness of such a refinement requires generating and verifying additional proof obligations. We tackle this problem considering Java and UML/OCL as example. We present a sequent calculus for Java integer arithmetic with integrated generation of refinement proof obligations. Thus, there is no explicit refinement relation, such that the arising complications remain (as far as possible) hidden from the user. Our approach has been implemented as part of the KeY system.

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. Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  2. Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY Tool. Software and System Modeling, 1–42 (2004) (to appear)

    Google Scholar 

  3. Ahrendt, W., Baar, T., Beckert, B., Giese, M., Habermalz, E., Hähnle, R., Menzel, W., Schmitt, P.H.: The KeY approach: Integrating object oriented design and formal verification. In: Brewka, G., Moniz Pereira, L., Ojeda-Aciego, M., de Guzmán, I.P. (eds.) JELIA 2000. LNCS (LNAI), vol. 1919, p. 21. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  4. Beckert, B.: A dynamic logic for the formal verification of Java Card programs. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol. 2041, pp. 6–24. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  5. Beckert, B., Keller, U., Schmitt, P.H.: Translating the Object Constraint Language into first-order predicate logic. In: Proceedings, VERIFY, Workshop at Federated Logic Conferences (FLoC), Copenhagen, Denmark (2002), Available at: http://www.key-project.org/doc/2002/BeckertKellerSchmitt02.ps.gz

  6. Cataño, N., Huisman, M.: Formal specification and static checking of Gemplus’ electronic purse using ESC/Java. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 272–289. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  7. Chalin, P.: Improving JML: For a Safer and More Effective Language. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, Springer, Heidelberg (2003)

    Google Scholar 

  8. ESC/Java (Extended Static Checking for Java), http://research.compaq.com/SRC/esc/

  9. European Space Agency. Ariane 501 inquiry board report (July 1996), Available at: http://ravel.esrin.esa.it/docs/esa-x-1819eng.pdf

  10. Glesner, S.: Java Card Integer Arithmetic: About an Inconsistency and Its Algebraic Reason, Draft (2004)

    Google Scholar 

  11. Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 2nd edn. Addison-Wesley, Reading (2000)

    Google Scholar 

  12. Harrison, J.: A machine-checked theory of floating point arithmetic. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 113–130. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  13. Harrison, J.: Formal verification of IA-64 division algorithms. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 234–251. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  14. He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187–196. Springer, Heidelberg (1986)

    Google Scholar 

  15. Huisman, M.: Java Program Verification in Higher-Order Logic with PVS and Isabelle. PhD thesis, University of Nijmegen, The Netherlands (2001)

    Google Scholar 

  16. Jacobs, B.: Java’s Integral Types in PVS. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 1–15. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  17. Kit, B.: Available at: http://www.gemplus.com/smart/r_d/publications/case-study/

  18. Leavens, G.T., Baker, A.L., Ruby, C.: JML: A Notation for Detailed Design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 175–188. Kluwer, Dordrecht (1999)

    Google Scholar 

  19. Object Management Group, Inc., Framingham/MA, USA. OMG Unified Modeling Language Specification, Version 1.3 (June 1999), http://www.omg.org

  20. Poetzsch-Heffter, A., Müller, P.: A programming logic for sequential java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, p. 162. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  21. Schlager, S.: Handling of Integer Arithmetic in the Verification of Java Programs. Master’s thesis, Universität Karlsruhe (2002), Available at: http://www.key-project.org/doc/2002/DA-Schlager.ps.gz

  22. Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice Hall International Series in Computer Science (1992)

    Google Scholar 

  23. Stenzel, K.: Verification of JavaCard Programs. Technical report 2001-5, Institut für Informatik, Universität Augsburg, Germany (2001), Available at: http://www.informatik.uni-augsburg.de/swt/fmg/papers/

  24. Stump, A., Barrett, C.W., Dill, D.L.: CVC: A Cooperating Validity Checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 500–504. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  25. von Oheimb, D.: Analyzing Java in Isabelle/HOL: Formalization, Type Safety and Hoare Logic. PhD thesis, Technische Universität München (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for Computer Science, University of Koblenz-Landau, D-56072, Koblenz, Germany

    Bernhard Beckert

  2. Institute for Logic, Complexity and Deduction Systems, University of Karlsruhe, D-76128, Karlsruhe, Germany

    Steffen Schlager

Authors
  1. Bernhard Beckert
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Steffen Schlager
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computing Laboratory, University of Kent, CT2 7NF, Canterbury, Kent, UK

    Eerke A. Boiten

  2. Department of Computing, University of Sheffield, S1 4DP, Sheffield, UK

    John Derrick

  3. School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Australia

    Graeme Smith

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Beckert, B., Schlager, S. (2004). Software Verification with Integrated Data Type Refinement for Integer Arithmetic. In: Boiten, E.A., Derrick, J., Smith, G. (eds) Integrated Formal Methods. IFM 2004. Lecture Notes in Computer Science, vol 2999. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24756-2_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24756-2_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-21377-2

  • Online ISBN: 978-3-540-24756-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation