Advertisement

On Models and Code

A Unified Approach to Support Large-Scale Deductive Program Verification
  • Marieke HuismanEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11244)

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.

Notes

Acknowledgements

The author is supported by NWO VICI 639.023.710 Mercedes project.

References

  1. 1.
    Abrial, J.-R.: Modeling in Event-B – System and Software Engineering. Cambridge University Press (2010)Google Scholar
  2. 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. 3.
    Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. LMCS 11(1) (2015)Google Scholar
  4. 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_1CrossRefGoogle Scholar
  5. 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_33CrossRefGoogle Scholar
  6. 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. 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. 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. 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. 10.
    Dawes, J.: The VDM-SL Reference Guide. Pitman (1991)Google Scholar
  11. 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_16CrossRefGoogle Scholar
  12. 12.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRefGoogle Scholar
  13. 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. 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. 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–1Google Scholar
  16. 16.
    International Organisation for Standardization. Information technology–Z Formal Specification Notation-Syntax, Type System and Semantics (2000). ISO/IEC 13568:2002Google Scholar
  17. 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. 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. 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. 20.
    Meyer, B.: Object-Oriented Software Construction, 2nd Edn. Prentice-Hall (1997)Google Scholar
  21. 21.
    O’Hearn, P.W.: Resources, concurrency and local reasoning. Theor. Comput. Sci. 375(1–3), 271–307 (2007)MathSciNetCrossRefGoogle Scholar
  22. 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_58CrossRefGoogle Scholar
  23. 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_12CrossRefGoogle Scholar
  24. 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-2CrossRefGoogle Scholar
  25. 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_21CrossRefGoogle Scholar
  26. 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)CrossRefGoogle Scholar
  27. 27.
    Zaharieva-Stojanovski, M.: Closer to reliable software: verifying functional behaviour of concurrent programs. Ph.D. thesis, University of Twente (2015)Google Scholar
  28. 28.
    Zhang, D.: From concurrent state machines to reliable multi-threaded Java code. Ph.D. thesis, Technische Universiteit Eindhoven (2018)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.University of TwenteEnschedeThe Netherlands

Personalised recommendations