Abstract
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 is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Cheon, Y., Perumandla, A.: Specifying and checking method call sequences of Java programs. Softw. Qual. Control. 15(1), 7–25 (2007)
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 2017
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)
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)
Meyer, B.: Applying “design by contract”. Computer 25(10), 40–51 (1992)
Sousa, D.G., Dias, R.J., Ferreira, C., Lourenço, J.M.: Preventing atomicity violations with contracts. arXiv preprint arXiv:1505.02951, May 2015
Acknowledgments
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).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Lourenço, J.M. (2018). Verifying Real-World Software with Contracts for Concurrency. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice. ISoLA 2018. Lecture Notes in Computer Science(), vol 11247. Springer, Cham. https://doi.org/10.1007/978-3-030-03427-6_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-03427-6_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-03426-9
Online ISBN: 978-3-030-03427-6
eBook Packages: Computer ScienceComputer Science (R0)