Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Verification of Object-Oriented Software

FoVeOOS 2010: Formal Verification of Object-Oriented Software pp 168–182Cite as

A Dynamic Logic for Unstructured Programs with Embedded Assertions

  • Conference paper

  • 454 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6528))

Abstract

We present a program logic for an intermediate verification programming language and provide formal definitions of its syntax and semantics. The language is unstructured, indeterministic, and has embedded assertions. A set of sound rewrite rules which allow symbolic execution of programs is given. We prove the soundness of three inference rules using invariants which can be used to deal with loops during the verification.

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. Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Ernst, M.D., Jensen, T.P. (eds.) PASTE 2005, pp. 82–87. ACM Press, New York (2005)

    Google Scholar 

  2. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)

    Google Scholar 

  3. Beckert, B., Schlager, S., Schmitt, P.H.: An improved rule for while loops in deductive program verification. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 315–329. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  4. Böhme, S., Leino, K.R.M., Wolff, B.: HOL-boogie — an interactive prover for the boogie program-verifier. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 150–166. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  5. Burdy, L., Pavlova, M.: Java bytecode specification and verification. In: Liebrock, L.M. (ed.) SAC 2006. ACM, New York (2006)

    Google Scholar 

  6. DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research, Redmond (2005)

    Google Scholar 

  7. Dennis, G., Chang, F.S.-H., Jackson, D.: Modular verification of code with SAT. In: Pollock, L.L., Pezzè, M. (eds.) ISSTA 2006, pp. 109–120. ACM Press, New York (2006)

    Google Scholar 

  8. Filliâtre, J.-C., Marché, C.: The why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  9. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)

    MATH  Google Scholar 

  10. Leino, K.R.M.: This is Boogie 2, Manuscript KRML 178 (2008), http://research.microsoft.com/~leino/papers.html

  11. Leino, K.R.M., Rümmer, P.: A polymorphic intermediate verification language: Design and logical encoding. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 312–327. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  12. Quigley, C.L.: A programming logic for java bytecode programs. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 41–54. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  13. Sinz, C., Falke, S., Merz, F.: A precise memory model for low-level bounded model checking. In: Huuck, R., Klein, G., Schlich, B. (eds.) SSV 2010 (2010)

    Google Scholar 

  14. Stenzel, K.: Verification of Java Card Programs. PhD thesis, University of Augsburg (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for Theoretical Computer Science, Karlsruhe Institute of Technology, D-76128, Karlsruhe, Germany

    Mattias Ulbrich

Authors
  1. Mattias Ulbrich
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute for Theoretical Informatics, Am Fasanengarten 5, 76131, Karlsruhe, Germany

    Bernhard Beckert

  2. INRIA Saclay- Île-de-France, Parc Orsay Université, 4 rue Jacques Monod, 91893, Orsay Cedex, France

    Claude Marché

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ulbrich, M. (2011). A Dynamic Logic for Unstructured Programs with Embedded Assertions. In: Beckert, B., Marché, C. (eds) Formal Verification of Object-Oriented Software. FoVeOOS 2010. Lecture Notes in Computer Science, vol 6528. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-18070-5_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-18070-5_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-18069-9

  • Online ISBN: 978-3-642-18070-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation