Skip to main content
SpringerLink
Log in

Dynamic Frames Based Verification Method for Concurrent Java Programs

  • Conference paper
Verified Software: Theories, Tools, and Experiments (VSTTE 2015)

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

Included in the following conference series:

Abstract

In this paper we discuss a verification method for concurrent Java programs based on the concept of dynamic frames. We build on our earlier work that proposes a new, symbolic permission system for concurrent reasoning and we provide the following new contributions. First, we describe our approach for proving program specifications to be self-framed with respect to permissions, which is a necessary condition to maintain soundness in concurrent reasoning. Second, we show how we use predicates to provide modular and reusable specifications for program synchronisation points, like locks or forked threads. Our work primarily targets the KeY verification system with its specification language JML⁎ and symbolic execution proving method. Hence, we also give the current status of the work on implementation and we discuss some examples that are verifiable with KeY.

This work is supported by ERC grant 258405 for the VerCors project and by the Swedish Knowledge Foundation grant for the AUTO-CAAS project.

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 EPUB and 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

Notes

  1. 1.

    http://fmt.cs.utwente.nl/research/projects/VerCors/.

  2. 2.

    http://www.key-project.org/.

  3. 3.

    Although locks are actually not threads, classifying them as such allows us to suitably generalise the symbolic permission approach.

  4. 4.

    This problem is common in permission-based approaches and makes reasoning about functional behaviour of concurrent programs difficult. Solutions exist to enable to keep certain information about temporarily inaccessible locations [16], however, they are beyond the scope of this paper, here we concentrate on the basic soundness of dynamic frames enriched with permissions.

  5. 5.

    Available at http://www.key-project.org/download/.

  6. 6.

    This is not the most elegant way of passing specifications (predicates) around classes in JML⁎, however, a working one and currently the only one that the KeY implementation allows. In the future we plan to provide proper ghost and model parameters to classes and methods in the style of [22].

References

  1. Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  2. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science, pp. 55–74. IEEE Computer Society (2002)

    Google Scholar 

  3. Leino, K.R.M., Müller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007/2008/2009. LNCS, vol. 5705, pp. 195–222. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  4. Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 439–458. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  5. Amighi, A., Blom, S., Darabi, S., Huisman, M., Mostowski, W., Zaharieva-Stojanovski, M.: Verification of concurrent systems with VerCors. In: Bernardo, M., Damiani, F., Hähnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 172–216. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  6. Kassios, I.T.: Dynamic frames: support for framing, dependencies and sharing without restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268–283. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  7. Schmitt, P.H., Ulbrich, M., Weiß, B.: Dynamic frames in Java dynamic logic. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 138–152. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  8. Ahrendt, W., Beckert, B., Bruns, D., Bubel, R., Gladisch, C., Grebing, S., Hähnle, R., Hentschel, M., Herda, M., Klebanov, V., Mostowski, W., Scheben, C., Schmitt, P.H., Ulbrich, M.: The KeY platform for verification and analysis of Java programs. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 55–71. Springer, Heidelberg (2014)

    Google Scholar 

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

    Article  Google Scholar 

  10. Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 127–131. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  11. Huisman, M., Mostowski, W.: A symbolic approach to permission accounting for concurrent reasoning. In: 14th International Symposium on Parallel and Distributed Computing (ISPDC 2015), pp. 165–174. IEEE Computer Society (2015)

    Google Scholar 

  12. Mostowski, W.: A case study in formal verification using multiple explicit heaps. In: Beyer, D., Boreale, M. (eds.) FMOODS/FORTE 2013. LNCS, vol. 7892, pp. 20–34. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  13. Mostowski, W., Ulbrich, M.: Dynamic dispatch for method contracts through abstract predicates. In: 15th International Conference on MODULARITY, pp. 109–116. ACM (2015)

    Google Scholar 

  14. Beckert, B., Schmitt, P.H.: Program verification using change information. In: Proceedings, Software Engineering and Formal Methods (SEFM) 2003, pp. 91–99. IEEE Press (2003)

    Google Scholar 

  15. Bruns, D., Mostowski, W., Ulbrich, M.: Implementation-level verification of algorithms with KeY. Softw. Tools Technol. Transf. 17(6), 729–744 (2013)

    Article  Google Scholar 

  16. Blom, S., Huisman, M., Zaharieva-Stojanovski, M.: History-based verification of functional behaviour of concurrent programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 84–98. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  17. Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 348–370. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  18. Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Palsberg, J., Abadi, M. (eds.) Principles of Programming Languages, pp. 259–270. ACM (2005)

    Google Scholar 

  19. Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. Logical Methods Comput. Sci. 11, 1–66 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  20. O’Hearn, P.W.: Resources, concurrency and local reasoning. Theor. Comput. Sci. 375(1–3), 271–307 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  21. Blom, S., Huisman, M., Kiniry, J.: How do developers use APIs? A case study in concurrency. In: International Conference on Engineering of Complex Computer Systems, pp. 212–221. IEEE Computer Society (2013)

    Google Scholar 

  22. Amighi, A., Blom, S., Huisman, M., Mostowski, W., Zaharieva-Stojanovski, M.: Formal specifications for Java’s synchronisation classes. In: Lafuente, A.L., Tuosto, E. (eds.) 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, pp. 725–733. IEEE Computer Society (2014)

    Google Scholar 

  23. Haack, C., Hurlin, C.: Separation logic contracts for a Java-like language with fork/join. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 199–215. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  24. Boyland, J., Müller, P., Schwerhoff, M., Summers, A.J.: Constraint semantics for abstract read permissions. In: Formal Techniques for Java-Like Programs (FTfJP). ACM (2014)

    Google Scholar 

  25. Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  26. Juhasz, U., Kassios, I.T., Müller, P., Novacek, M., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. Technical report, ETH Zürich (2014)

    Google Scholar 

  27. Bao, Y., Leavens, G.T., Ernst, G.: Translating separation logic into dynamic frames using fine-grained region logic. Technical report CS-TR-13-02a, Computer Science, University of Central Florida, March 2014

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Formal Methods and Tools, University of Twente, Enschede, The Netherlands

    Wojciech Mostowski

  2. Center for Research on Embedded Systems, Halmstad University, Halmstad, Sweden

    Wojciech Mostowski

Authors
  1. Wojciech Mostowski
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wojciech Mostowski .

Editor information

Editors and Affiliations

  1. Software Engineering Institute, Carnegie Mellon University, Pittsburgh, PA, USA

    Arie Gurfinkel

  2. Department of Electrical Engineering and Computer Science, University of California, Berkeley, USA

    Sanjit A. Seshia

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Mostowski, W. (2016). Dynamic Frames Based Verification Method for Concurrent Java Programs. In: Gurfinkel, A., Seshia, S.A. (eds) Verified Software: Theories, Tools, and Experiments. VSTTE 2015. Lecture Notes in Computer Science(), vol 9593. Springer, Cham. https://doi.org/10.1007/978-3-319-29613-5_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-29613-5_8

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-29612-8

  • Online ISBN: 978-3-319-29613-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation