Verifying Concurrent Programs Using Contracts

Ricardo J. Dias, Carla Ferreira, Jan Fiedor, Joao M. Lourenco, Ales Smrcka, Diogo G. Sousa, Tomas Vojnar

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)

Abstract

The central notion of this paper is that of contracts for concurrency, allowing one to capture the expected atomicity of sequences of method or service calls in a concurrent program. The contracts may be either extracted automatically from the source code, or provided by developers of libraries or software modules to reflect their expected usage in a concurrent setting. We start by extending the so-far considered notion of contracts for concurrency in several ways, improving their expressiveness and enhancing their applicability in practice. Then, we propose two complementary analyses - a static and a dynamic one - to verify programs against the extended contracts. We have implemented both approaches and present promising experimental results from their application on various programs, including real-world ones where our approach unveiled previously unknown errors.

Original languageEnglish
Title of host publicationProceedings - 10th IEEE International Conference on Software Testing, Verification and Validation, ICST 2017
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages196-206
Number of pages11
ISBN (Electronic)978-1-5090-6031-3
DOIs
Publication statusPublished - 15 May 2017
Event10th IEEE International Conference on Software Testing, Verification and Validation, ICST 2017 - Tokyo, Japan
Duration: 13 Mar 201717 Mar 2017

Conference

Conference10th IEEE International Conference on Software Testing, Verification and Validation, ICST 2017
CountryJapan
CityTokyo
Period13/03/1717/03/17

Keywords

  • Atomicity violation
  • Concurrency
  • Contracts
  • Dynamic analysis
  • Noise injection
  • Order violation
  • Static analysis

Cite this

Dias, R. J., Ferreira, C., Fiedor, J., Lourenco, J. M., Smrcka, A., Sousa, D. G., & Vojnar, T. (2017). Verifying Concurrent Programs Using Contracts. In Proceedings - 10th IEEE International Conference on Software Testing, Verification and Validation, ICST 2017 (pp. 196-206). [7927975] Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ICST.2017.25