Skip to main content
SpringerLink
Log in

On Models and Code

A Unified Approach to Support Large-Scale Deductive Program Verification

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation. Modeling (ISoLA 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11244))

Included in the following conference series:

Abstract

Despite the substantial progress in the area of deductive program verification over the last years, it still remains a challenge to use deductive verification on large-scale industrial applications. In this abstract, I analyse why this is case, and I argue that in order to solve this, we need to soften the border between models and code. This has two important advantages: (1) it would make it easier to reason about high-level behaviour of programs, using deductive verification, and (2) it would allow to reason about incomplete applications during the development process. I discuss how the first steps towards this goal are supported by verification techniques within the VerCors project, and I will sketch the future steps that are necessary to realise this goal.

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.

    Of course, a similar argument can be made here, but the advantage is that if the annotated code is available, correctness can be reverified by other tools.

References

  1. Abrial, J.-R.: Modeling in Event-B – System and Software Engineering. Cambridge University Press (2010)

    Google Scholar 

  2. Amighi, A., Blom, S., Huisman, M.: VerCors: a layered approach to practical verification of concurrent software. In PDP, pp. 495–503 (2016)

    Google Scholar 

  3. Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. LMCS 11(1) (2015)

    Google Scholar 

  4. Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1–17. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19718-5_1

    Chapter  Google Scholar 

  5. Bjørner, D.: The vienna development method (VDM). In: Blum, E.K., Paul, M., Takasu, S. (eds.) Mathematical Studies of Information Processing. LNCS, vol. 75, pp. 326–359. Springer, Heidelberg (1979). https://doi.org/10.1007/3-540-09541-1_33

    Chapter  Google Scholar 

  6. Bowen, J.P., Olderog, E.-R., Fränzle, M., Ravn, A.P.: Developing correct systems. In: Fifth Euromicro Workshop on Real-Time Systems, RTS 1993, Oulu, Finland, 22–24 June 1993, Proceedings, pp. 176–187. IEEE (1993)

    Google Scholar 

  7. Brahmi, A., Delmas, D., Essousi, M.H., Randimbivololona, F., Atki, A., Marie, T.: Formalise to automate: deployment of a safe and cost-efficient process for avionics software. In: Embedded Real-Time Software and Systems (ERTS\(^2\)) (2018)

    Google Scholar 

  8. Burstall, R.M.: Program proving as hand simulation with a little induction. In: Information Processing 1974, pp. 308–312. Elsevier, North-Holland (1974)

    Google Scholar 

  9. Dalvandi, M., Butler, M.J., Rezazadeh, A.: Transforming Event-B models to Dafny contracts. In: Proceedings of the 15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015), Volume 72 of Electronic Communications of the EASST (2015)

    Google Scholar 

  10. Dawes, J.: The VDM-SL Reference Guide. Pitman (1991)

    Google Scholar 

  11. de Gouw, S., Rot, J., de Boer, F.S., Bubel, R., Hähnle, R.: OpenJDK’s Java.utils.Collection.sort() is broken: the good, the bad and the worst case. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 273–289. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_16

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  13. Huisman, M., Blom, S., Darabi, S., Safari, M.: Program correctness by transformation. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11244, pp. 365–380. Springer, Cham (2018)

    Google Scholar 

  14. Huisman, M., Klebanov, V., Monahan, R., Tautschnig, M.: VerifyThis 2015 a program verification competition. Int. J. Softw. Tools Technol. Transfer (2016)

    Google Scholar 

  15. International Organisation for Standardization. Information technology–Programming languages, their environments and system software interfaces–Vienna Development Method-Specification Language–Part 1: Base language, December 1996. ISO/IEC 13817–1

    Google Scholar 

  16. International Organisation for Standardization. Information technology–Z Formal Specification Notation-Syntax, Type System and Semantics (2000). ISO/IEC 13568:2002

    Google Scholar 

  17. Joosten, S.J.C., Oortwijn, W., Safari, M., Huisman, M.: An exercise in verifying sequential programs with VerCors. In: Summers, A.J. (ed.) 20th Workshop on Formal Techniques for Java-like Programs (FTfJP) (2018)

    Google Scholar 

  18. Jung, R., et al.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: POPL, pp. 637–650. ACM (2015)

    Google Scholar 

  19. Kästner, D., et al.: CompCert: practical experience on integrating and qualifying a formally verified optimizing compiler. In: ERTS 2018: Embedded Real Time Software and Systems. SEE (2018)

    Google Scholar 

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

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  22. Olderog, E.-R., Rössig, S.: A case study in transformational design of concurrent systems. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993. LNCS, vol. 668, pp. 90–104. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56610-4_58

    Chapter  Google Scholar 

  23. Oortwijn, W., Blom, S., Gurov, D., Huisman, M., Zaharieva-Stojanovski, M.: An abstraction technique for describing concurrent program behaviour. In: Paskevich, A., Wies, T. (eds.) VSTTE 2017. LNCS, vol. 10712, pp. 191–209. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-72308-2_12

    Chapter  Google Scholar 

  24. Partsch, H.: Specification and Transformation of Programs - A Formal Approach to Software Development. Texts and Monographs in Computer Science. Springer, Heidelberg (1990). https://doi.org/10.1007/978-3-642-61512-2

  25. Penninckx, W., Mühlberg, J.T., Smans, J., Jacobs, B., Piessens, F.: Sound formal verification of Linux’s USB BP keyboard driver. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 210–215. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28891-3_21

    Chapter  Google Scholar 

  26. Tran-Jørgensen, P.W.V., Larsen, P.G., Leavens, G.T.: Automated translation of VDM to JML-annotated Java. STTT 20(2), 211–235 (2018)

    Article  Google Scholar 

  27. Zaharieva-Stojanovski, M.: Closer to reliable software: verifying functional behaviour of concurrent programs. Ph.D. thesis, University of Twente (2015)

    Google Scholar 

  28. Zhang, D.: From concurrent state machines to reliable multi-threaded Java code. Ph.D. thesis, Technische Universiteit Eindhoven (2018)

    Google Scholar 

Download references

Acknowledgements

The author is supported by NWO VICI 639.023.710 Mercedes project.

Author information

Authors and Affiliations

  1. University of Twente, Enschede, The Netherlands

    Marieke Huisman

Authors
  1. Marieke Huisman
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marieke Huisman .

Editor information

Editors and Affiliations

  1. University of Limerick, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Huisman, M. (2018). On Models and Code. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Modeling. ISoLA 2018. Lecture Notes in Computer Science(), vol 11244. Springer, Cham. https://doi.org/10.1007/978-3-030-03418-4_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-03418-4_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-03417-7

  • Online ISBN: 978-3-030-03418-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation