Verifying Real-World Software with Contracts for Concurrency

  • João M. LourençoEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11247)


In this paper we present Contracts for Concurrency. A contract for concurrency specifies the protocol to access the services provided by a software module or library. A program that respects a (well-defined and complete) contract for a module is safe from high-level atomicity violations with respect to that module. On the other hand, violations of a contract may denote errors in the program, and the application of contracts for concurrency to some real-world open source software packages did uncover a few latent bugs.



This paper describes work that was developed in collaboration with other colleagues from NOVA University Lisbon and Brno University of Technology [2, 6]. This work was partially supported by NOVA LINCS (UID/CEC/ 04516/2013) and the National Science Foundation (FCT/MEC) in the framework of the HiPsTr research project (02/SAICT/2017–032456).


  1. 1.
    Cheon, Y., Perumandla, A.: Specifying and checking method call sequences of Java programs. Softw. Qual. Control. 15(1), 7–25 (2007)CrossRefGoogle Scholar
  2. 2.
    Dias, R.J., et al.: Verifying concurrent programs using contracts. In: 2017 IEEE International Conference on Software Testing, Verification and Validation (ICST), pp. 196–206, March 2017Google Scholar
  3. 3.
    Hurlin, C.: Specifying and checking protocols of multithreaded classes. In: Proceedings of the 2009 ACM Symposium on Applied Computing, SAC 2009, pp. 587–592. ACM, New York (2009)Google Scholar
  4. 4.
    Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. SIGPLAN Not. 43(3), 329–339 (2008)CrossRefGoogle Scholar
  5. 5.
    Meyer, B.: Applying “design by contract”. Computer 25(10), 40–51 (1992)CrossRefGoogle Scholar
  6. 6.
    Sousa, D.G., Dias, R.J., Ferreira, C., Lourenço, J.M.: Preventing atomicity violations with contracts. arXiv preprint arXiv:1505.02951, May 2015

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.NOVA LINCS—NOVA Laboratory for Computer Science and Informatics, Departamento de Informática, Faculdade de Ciências e TecnologiaUniversidade Nova de LisboaCaparicaPortugal

Personalised recommendations