Conference paper| 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. | | Publication language: | english |
|---|
| Original title: | Verifying Concurrent Programs Using Contracts |
|---|
| Title (cs): | Verifikace paralelních programů pomocí kontraktů |
|---|
| 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) |
|---|
| Place: | Tokyo, JP |
|---|
| Year: | 2017 |
|---|
| ISBN: | 978-1-5090-6032-0 |
|---|
| DOI: | 10.1109/ICST.2017.25 |
|---|
| Publisher: | Institute of Electrical and Electronics Engineers |
|---|
| Keywords |
|---|
| contracts, concurrent computing, software, protocols, indexes, libraries, arrays |
| Annotation |
|---|
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. |
| BibTeX: |
|---|
@INPROCEEDINGS{
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 = {http://www.fit.vutbr.cz/research/view_pub.php.en.iso-8859-2?id=11510}
} |
|
Faculty of Information Technology