Skip to main content
SpringerLink
Log in

A Dynamic Logic for the Formal Verification ofJava Card Programs

  • Conference paper
  • First Online:
Java on Smart Cards:Programming and Security (JavaCard 2000)

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

Included in the following conference series:

Abstract

In this paper, we define a program logic (an instance of Dynamic Logic) for formalising properties of Java Card programs, and we give a sequent calculus for formally verifying such properties. The purpose of this work is to provide a framework for software verification that can be integrated into real-world software development processes.

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. W. Ahrendt, T. Baar, B. Beckert, M. Giese, E. Habermalz, R. Hähnle, W. Menzel, and P. H. Schmitt. The KeY approach: Integrating object oriented design and formal verification. In M. Ojeda-Aciego, I. P. de Guzman, G. Brewka, and L. M. Pereira, editors, Proceedings, Logics in Artificial Intelligence (JELIA), Malaga, Spain, LNCS 1919. Springer, 2000.

    Chapter  Google Scholar 

  2. J. Alves-Foss, editor. Formal Syntax and Semantics ofJava. LNCS 1523. Springer, 1999.

    Google Scholar 

  3. K. R. Apt. Ten years of Hoare logic: A survey-part I. ACM Transactions on Programming Languages and Systems, 1981.

    Google Scholar 

  4. T. Baar. Experiences with the UML/OCL-approach to precise software modeling: A report from practice. Available at i12www.ira.uka.de/~key, 2000.

    Google Scholar 

  5. E. Börger and W. Schulte. A programmer friendly modular definition of the semantics of Java. In Alves-Foss [2], pages 353–404.

    Google Scholar 

  6. C. Calcagno, S. Ishtiaq, and P. W. O’Hearn. Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic. In Proceedings, International Conference on Principles and Practice of De clarative Programming, Montreal, Canada. ACM, 2000.

    Google Scholar 

  7. E. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4):626–643, 1996.

    Article  Google Scholar 

  8. D. L. Dill and J. Rushby. Acceptance of formal methods: Lessons from hardware design. IEEE Computer, 29(4):23–24, 1996. Part of: Hossein Saiedian (ed.). An Invitation to Formal Methods. Pages 16-30.

    Google Scholar 

  9. J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specification. Addison Wesley, second edition, 2000.

    Google Scholar 

  10. M. G. Hinchey and J. P. Bowen, editors. Applications ofF ormal Methods. Prentice Hall, 1995.

    Google Scholar 

  11. M. Huisman and B. Jacobs. Java program verification via a Hoare logic with abrupt termination. In Proceedings, Fundamental Approaches to Software Engineering (FASE), Berlin, Germany, LNCS 1783. Springer, 2000.

    Chapter  Google Scholar 

  12. D. Hutter, B. Langenstein, C. Sengler, J. H. Siekmann, and W. Stephan. Deduction in the Verification Support Environment (VSE). In M.-C. Gaudel and J. Woodcock, editors, Proceedings, International Symposium ofF ormal Methods Europe (FME), Oxford, UK, LNCS 1051. Springer, 1996.

    Google Scholar 

  13. B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, and H. Tews. Reasoning about Java classes (preliminary report). In Proceedings, Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), pages 329–340. ACM Press, 1998.

    Google Scholar 

  14. D. Kozen and J. Tiuryn. Logic of programs. In J. van Leeuwen, editor, Handbook ofThe oretical Computer Science, volume B: Formal Models and Semantics, chapter 14, pages 789–840. Elsevier, Amsterdam, 1990.

    Google Scholar 

  15. J. Martin and J. J. Odell. Object-Oriented Methods: A Foundation, UML Edition. Prentice-Hall, 1997. 24 B. Beckert

    Google Scholar 

  16. T. Nipkow and D. von Oheimb. Machine-checking the Java specification: Proving type safety. In Alves-Foss [2], pages 119–156.

    Google Scholar 

  17. T. Nipkow, D. von Oheimb, and C. Pusch. µJava: Embedding a programming language in a theorem prover. In F. L. Bauer and R. Steinbrüggen, editors, Foundations ofSe cure Computation. IOS Press, 2000. To appear.

    Google Scholar 

  18. Object Management Group, Inc., Framingham/MA, USA, www.omg.org. OMG Unified Modeling Language Specification, Version 1.3, June 1999.

    Google Scholar 

  19. A. Poetzsch-Heffter and P. Müller. A programming logic for sequential Java. In S. D. Swierstra, editor, Proceedings, Programming Languages and Systems (ESOP), Amsterdam, The Netherlands, LNCS 1576, pages 162–176. Springer, 1999.

    Google Scholar 

  20. W. Reif.The KIV-approach to software verification. In M. Broy and S. Jähnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software-Final Report, LNCS 1009. Springer, 1995.

    Chapter  Google Scholar 

  21. D. von Oheimb. Axiomatic semantics for Javaight. In S. Drossopoulou, S. Eisenbach, B. Jacobs, G. T. Leavens, P. Müller, and A. Poetzsch-Heffter, editors, Proceedings, Formal Techniques for Java Programs, Workshop at ECOOP’00, Cannes, France, 2000.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Komplexit ät und DeduktionssystemeD-76128, Universität Karlsruhe Institut für Logik, Karlsruhe, Germany

    Bernhard Beckert

Authors
  1. Bernhard Beckert
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. INRIA Sophia Antipolis, 06902, Sophia Antipolis, Cedex, France

    Isabelle Attali

  2. IRISA/CNRS, Campus de Beaulieu, 35042, Rennes, France

    Thomas Jensen

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Beckert, B. (2001). A Dynamic Logic for the Formal Verification ofJava Card Programs. In: Attali, I., Jensen, T. (eds) Java on Smart Cards:Programming and Security. JavaCard 2000. Lecture Notes in Computer Science, vol 2041. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45165-X_2

Download citation

  • DOI: https://doi.org/10.1007/3-540-45165-X_2

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-45165-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation