Skip to main content
SpringerLink
Log in
Book cover

Brazilian Symposium on Formal Methods

SBMF 2013: Formal Methods: Foundations and Applications pp 99–114Cite as

Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking

  • Conference paper

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

Abstract

We show how to write a concise and elegant specification of a linearly linked data structure that is applicable for both verification and runtime checking. A specification of linked lists is given as an example. The concept of a list is captured by an observer method which is a functional version of a reachability predicate. The specification is written in the Java Modeling Language (JML) and does not require extensions of that language. This paper addresses a mixed audience of users and developers in the fields of formal verification, runtime checking, and specification language design. We provide an in-depth description of the proposed specification and analyze its implications both for verification and for runtime checking. Based on this analysis we have developed verification techniques that fully automate the verification process, using the KeY tool, and that are also described here.

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   49.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. Albert, E., Bubel, R., Genaim, S., Hähnle, R., Román-Díez, G.: Verified resource guarantees for heap manipulating programs. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 130–145. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  2. Becker, K., Leavens, G.T.: Class LinkedList, http://www.eecs.ucf.edu/~leavens/JML-release/javadocs/java/util/LinkedList.html#removeint

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

    Google Scholar 

  4. Beckert, B., Trentelman, K.: Second-order principles in specification languages for object-oriented programs. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 154–168. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Cheon, Y.: A quick tutorial on JET. Technical Report UTEP-CS-07-40, Department Technical Reports (CS), University of Texas at El Paso (June 2007)

    Google Scholar 

  6. Darvas, A., Müller, P.: Reasoning about method calls in interface specifications. Journal of Object Technology 5(5), 59–85 (2006)

    Article  Google Scholar 

  7. du Bousquet, L., Ledru, Y., Maury, O., Oriat, C., Lanet, J.-L.: Reusing a JML specification dedicated to verification for testing, and vice-versa: Case studies. Journal of Automated Reasoning 45, 415–435 (2010), 10.1007/s10817-009-9132-y

    Article  MathSciNet  Google Scholar 

  8. Jacobs, B., Piessens, F.: Inspector methods for state abstraction. Journal of Object Technology 6(5), 55–75 (2007)

    Article  Google Scholar 

  9. Jensen, J.B., Birkedal, L., Sestoft, P.: Modular verification of linked lists with views via separation logic. Journal of Object Technology 10(2), 1–20 (2011)

    Google Scholar 

  10. Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: Proceedings of POPL, pp. 115–126. ACM (2006)

    Google Scholar 

  11. Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SEN 31(3), 1–38 (2006)

    Google Scholar 

  12. Leavens, G.T., Leino, R., Müller, P.: Specification and verification challenges for sequential object-oriented programs. Formal Asp. Comput. 19(2), 159–189 (2007)

    Article  MATH  Google Scholar 

  13. Leino, K.R.M.: Specification and verification of object-oriented software. In: Engineering Methods and Tools for Software Safety and Security. NATO Science for Peace and Security, vol. 22, pp. 231–266. IOS Press (2009)

    Google Scholar 

  14. Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. Logical Methods in Computer Science 5(2) (2009)

    Google Scholar 

  15. Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 181–198. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  16. Nelson, G.: Verifying reachability invariants of linked structures. In: Proceedings of POPL, pp. 38–47. ACM (1983)

    Google Scholar 

  17. Nguyen, H.H., Kuncak, V., Chin, W.-N.: Runtime checking for separation logic. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 203–217. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Rajamani, S.K.: Verification, testing and statistics. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, p. 25. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  19. Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames: Combining dynamic frames and separation logic. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 148–172. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  20. Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: Proceedings of PLDI, pp. 349–361 (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for Theoretical Informatics, Karlsruhe Institute of Technology (KIT), Germany

    Christoph Gladisch

  2. School of Computer Science, The Academic College Tel Aviv-Yaffo, Israel

    Shmuel Tyszberowicz

Authors
  1. Christoph Gladisch
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Shmuel Tyszberowicz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Centro de Informática, UFPE, Recife, PE, Brazil

    Juliano Iyoda

  2. Microsoft Research, Redmond, WA, USA

    Leonardo de Moura

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gladisch, C., Tyszberowicz, S. (2013). Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking. In: Iyoda, J., de Moura, L. (eds) Formal Methods: Foundations and Applications. SBMF 2013. Lecture Notes in Computer Science, vol 8195. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41071-0_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-41071-0_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-41070-3

  • Online ISBN: 978-3-642-41071-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation