Skip to main content
SpringerLink
Log in

Verification of Concurrent Systems with VerCors

  • Chapter
Formal Methods for Executable Software Models (SFM 2014)

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

Abstract

This paper presents the VerCors approach to verification of concurrent software. It first discusses why verification of concurrent software is important, but also challenging. Then it shows how within the VerCors project we use permission-based separation logic to reason about multithreaded Java programs. We discuss in particular how we use the logic to use different implementations of synchronisers in verification, and how we reason about class invariance properties in a concurrent setting. Further, we also show how the approach is suited to reason about programs using a different concurrency paradigm, namely kernel programs using the Single Instruction Multiple Data paradigm. Concretely, we illustrate how permission-based separation logic is suitable to verify functional correctness properties of OpenCL kernels. All verification techniques discussed in this paper are supported by the VerCors tool set.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 16.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. Amighi, A., Blom, S., Huisman, M.: Resource protection using atomics: Patterns and verifications. Technical Report TR-CTIT-13-10, CTIT, University of Twente (2013)

    Google Scholar 

  2. 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 

  3. Apt, K.R.: Ten years of Hoare’s logic: A survey – Part I. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981)

    Article  MATH  Google Scholar 

  4. Artho, C., Havelund, K., Biere, A.: High-level data races. Softw. Test., Verif. Reliab. 13(4), 207–227 (2003)

    Article  Google Scholar 

  5. Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6), 27–56 (2004)

    Article  Google Scholar 

  6. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

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

    Google Scholar 

  8. Berdine, J., Calcagno, C., O’Hearn, P.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  9. Betts, A., Chong, N., Donaldson, A., Qadeer, S., Thomson, P.: GPUVerify: A verifier for GPU kernels. In: Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2012, pp. 113–132. ACM, New York (2012)

    Chapter  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. Blom, S., Huisman, M., Mihelčić, M.: Specification and verification of GPGPU programs. Accepted to appear in Science of Computer Programming (2013)

    Google Scholar 

  12. 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 

  13. Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Software Tools for Technology Transfer 7, 212–232 (2005)

    Article  Google Scholar 

  14. Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and ESC/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342–363. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  15. Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  16. Cohen, E., Moskal, M., Schulte, W., Tobies, S.: Local verification of global invariants in concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 480–494. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  17. Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472–479. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  18. Cowan, B., Kapralos, B.: GPU-based acoustical occlusion modeling with acoustical texture maps. In: Proceedings of the 6th Audio Mostly Conference: A Conference on Interaction with Sound, AM 2011, pp. 55–61. ACM, New York (2011)

    Google Scholar 

  19. Dietl, W., Müller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology 4(8), 5–32 (2005)

    Article  Google Scholar 

  20. Dietl, W., Müller, P.: Object ownership in program verification. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. LNCS, vol. 7850, pp. 289–318. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  21. DiStefano, D., Parkinson, M.: jStar: Towards practical verification for Java. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications, pp. 213–226. ACM (2008)

    Google Scholar 

  22. Drossopoulou, S., Francalanza, A., Müller, P., Summers, A.J.: A unified framework for verification techniques for object invariants. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 412–437. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  23. Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering 27(2), 99–123 (2001)

    Article  Google Scholar 

  24. Floyd, R.W.: Assigning meanings to programs. Proc. Symp. Appl. Math. 19, 19–31 (1967)

    Article  MathSciNet  MATH  Google Scholar 

  25. Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 19–37. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  26. Haack, C., Huisman, M., Hurlin, C.: Reasoning about Java’s reentrant locks. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 171–187. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  27. Haack, C., Huisman, M., Hurlin, C., Amighi, A.: Permission-based separation logic for Java. Submitted to Logical Methods in Computer Science

    Google Scholar 

  28. Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  29. Hobor, A., Gherghina, C.: Barriers in concurrent separation logic. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 276–296. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  30. Huisman, M., Mihelčić, M.: Specification and verification of GPGPU programs using permission-based separation logic. In: BYTECODE 2013 (2013)

    Google Scholar 

  31. Huizing, K., Kuiper, R.: Verification of object oriented programs using class invariants. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 208–221. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  32. Jacobs, B., Piessens, F., Leino, K.R.M., Schulte, W.: Safe concurrency for aggregate objects with invariants. In: Software Engineering and Formal Methods, pp. 137–147 (2005)

    Google Scholar 

  33. 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 

  34. Jason Sanders, E.K.: CUDA by Example: An Introduction to General-Purpose GPU Programming. Addison-Wesley Professional (2010)

    Google Scholar 

  35. Khronos OpenCL Working Group. The OpenCL specification (2008-2013)

    Google Scholar 

  36. Leavens, G., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., Müller, P., Kiniry, J., Chalin, P.: JML Reference Manual. Dept. of Computer Science, Iowa State University (February 2007), http://www.jmlspecs.org

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

    Google Scholar 

  38. Leino, K.R.M.: This is Boogie 2. Technical report, Microsoft Research (June 2008)

    Google Scholar 

  39. 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 

  40. Li, G., Gopalakrishnan, G.: Scalable SMT-based verification of GPU kernel functions. In: SIGSOFT FSE 2010, Santa Fe, NM, USA, pp. 187–196. ACM (2010)

    Google Scholar 

  41. Liskov, B., Guttag, J.: Abstraction and specification in program development. MIT Press, Cambridge (1986)

    MATH  Google Scholar 

  42. Lu, Y., Potter, J., Xue, J.: Validity invariants and effects. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 202–226. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  43. Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall (1997)

    Google Scholar 

  44. Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Sci. Comput. Program. 62(3), 253–286 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  45. Mulligan, J.B.: A GPU-accelerated software eye tracking system. In: Proceedings of the Symposium on Eye Tracking Research and Applications, ETRA 2012, pp. 265–268. ACM, New York (2012)

    Google Scholar 

  46. O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science 375(1-3), 271–307 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  47. The OpenCL 1.2 specification (2011)

    Google Scholar 

  48. Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica Journal 6, 319–340 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  49. Parkinson, M.: Local reasoning for Java. Technical Report UCAM-CL-TR-654, University of Cambridge (2005)

    Google Scholar 

  50. Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 247–258. ACM (2005)

    Google Scholar 

  51. Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. Logical Methods in Computer Science 8(3:01), 1–54 (2012)

    MathSciNet  MATH  Google Scholar 

  52. Parr, T.: The Definitive ANTLR 4 Reference. Pragmatic Bookshelf (2013)

    Google Scholar 

  53. Poetzsch-Heffter, A.: Specification and Verification of Object-Oriented Programs. PhD thesis, Habilitation thesis, Technical University of Munich (1997)

    Google Scholar 

  54. Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction—A Basis for Applications, vol. II.1, pp. 13–39. Kluwer (1998)

    Google Scholar 

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

    Google Scholar 

  56. Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. ACM Trans. Program. Lang. Syst. 34(1) (2012)

    Google Scholar 

  57. Stone, S.S., Haldar, J.P., Tsao, S.C., Hwu, W.-M.W., Liang, Z.-P., Sutton, B.P.: Accelerating advanced MRI reconstructions on GPU-s. In: Proceedings of the 5th Conference on Computing Frontiers, CF 2008, pp. 261–272. ACM, New York (2008)

    Chapter  Google Scholar 

  58. VerCors project homepage (2014), http://www.utwente.nl/vercors/

  59. Weiß, B.: Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction. PhD thesis, Karlsruhe Institute of Technology (2011)

    Google Scholar 

  60. Zaharieva-Stojanovski, M., Huisman, M.: Verifying class invariants in concurrent programs. In: Gnesi, S., Rensink, A. (eds.) FASE 2014 (ETAPS). LNCS, vol. 8411, pp. 230–245. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Twente, The Netherlands

    Afshin Amighi, Stefan Blom, Saeed Darabi, Marieke Huisman, Wojciech Mostowski & Marina Zaharieva-Stojanovski

Authors
  1. Afshin Amighi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefan Blom
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Saeed Darabi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Marieke Huisman
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Wojciech Mostowski
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Marina Zaharieva-Stojanovski
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Scienze di Base e Fondamenti, Università di Urbino, Piazza della Republica 13, 61029, Urbino, Italy

    Marco Bernardo

  2. Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, 10149, Torino, Italy

    Ferruccio Damiani

  3. Fachbereich Informatik, Technische Universität Darmstadt, Hochschulstraße 10, 64289, Darmstadt, Germany

    Reiner Hähnle

  4. Department of Informatics, University of Oslo, P.O. Box 1080 Blindern, 0316, Oslo, Norway

    Einar Broch Johnsen

  5. Institut für Softwaretechnik und Fahrzeuginformatik, Technische Universität Braunschweig, Mühlenpfordtstraße 23, 38106, Braunschweig, Germany

    Ina Schaefer

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Amighi, A., Blom, S., Darabi, S., Huisman, M., Mostowski, W., Zaharieva-Stojanovski, M. (2014). Verification of Concurrent Systems with VerCors. In: Bernardo, M., Damiani, F., Hähnle, R., Johnsen, E.B., Schaefer, I. (eds) Formal Methods for Executable Software Models. SFM 2014. Lecture Notes in Computer Science, vol 8483. Springer, Cham. https://doi.org/10.1007/978-3-319-07317-0_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-07317-0_5

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-07316-3

  • Online ISBN: 978-3-319-07317-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation