Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Leveraging Applications of Formal Methods

ISoLA 2018: Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice pp 70–73Cite as

Verifying Real-World Software with Contracts for Concurrency

  • Conference paper
  • First Online:

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

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.

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

Learn about institutional subscriptions

Notes

  1. 1.

    https://issues.apache.org/bugzilla/show_bug.cgi?id=56784.

  2. 2.

    https://issues.apache.org/jira/browse/DERBY-6679.

  3. 3.

    https://issues.apache.org/jira/browse/CASSANDRA-7757.

References

  1. Cheon, Y., Perumandla, A.: Specifying and checking method call sequences of Java programs. Softw. Qual. Control. 15(1), 7–25 (2007)

    Article  Google Scholar 

  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 2017

    Google Scholar 

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

    Article  Google Scholar 

  5. Meyer, B.: Applying “design by contract”. Computer 25(10), 40–51 (1992)

    Article  Google Scholar 

  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

Download references

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

  1. NOVA LINCS—NOVA Laboratory for Computer Science and Informatics, Departamento de Informática, Faculdade de Ciências e Tecnologia, Universidade Nova de Lisboa, 2829-516, Caparica, Portugal

    João M. Lourenço

Authors
  1. João M. Lourenço
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to João M. Lourenço .

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

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)

Publish with us

Policies and ethics

Search

Navigation