Publication Details

Verifying Concurrent Programs Using Contracts

DIAS Ricardo J., FERREIRA Carla, FIEDOR Jan, LOURENCO Joao, SMRČKA Aleš, SOUSA Diogo J. and VOJNAR Tomáš. Verifying Concurrent Programs Using Contracts. In: 2017 IEEE International Conference on Software Testing, Verification and Validation (ICST). Tokyo: Institute of Electrical and Electronics Engineers, 2017, pp. 196-206. ISBN 978-1-5090-6032-0.
Czech title
Verifikace paralelních programů pomocí kontraktů
Type
conference paper
Language
english
Authors
Dias Ricardo J. (UNL)
Ferreira Carla (UNL)
Fiedor Jan, Ing., Ph.D. (DITS FIT BUT)
Lourenco Joao (UNL)
Smrčka Aleš, Ing., Ph.D. (DITS FIT BUT)
Sousa Diogo J. (UNL)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Keywords

contracts, concurrent computing, software, protocols, indexes, libraries, arrays

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.

Published
2017
Pages
196-206
Proceedings
2017 IEEE International Conference on Software Testing, Verification and Validation (ICST)
Conference
10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017), Tokyo, JP
ISBN
978-1-5090-6032-0
Publisher
Institute of Electrical and Electronics Engineers
Place
Tokyo, JP
DOI
UT WoS
000403393600018
EID Scopus
BibTeX
@INPROCEEDINGS{FITPUB11510,
   author = "J. Ricardo Dias and Carla Ferreira and Jan Fiedor and Joao Lourenco and Ale\v{s} Smr\v{c}ka and J. Diogo Sousa and Tom\'{a}\v{s} Vojnar",
   title = "Verifying Concurrent Programs Using Contracts",
   pages = "196--206",
   booktitle = "2017 IEEE International Conference on Software Testing, Verification and Validation (ICST)",
   year = 2017,
   location = "Tokyo, JP",
   publisher = "Institute of Electrical and Electronics Engineers",
   ISBN = "978-1-5090-6032-0",
   doi = "10.1109/ICST.2017.25",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11510"
}
Back to top