Detail publikace

Verifying Concurrent Programs Using Contracts

FIEDOR, J. VOJNAR, T. SMRČKA, A. DIAS, R. FERREIRA, C. LOURENCO, J. SOUSA, D.

Originální název

Verifying Concurrent Programs Using Contracts

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

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

Autoři

FIEDOR, J.; VOJNAR, T.; SMRČKA, A.; DIAS, R.; FERREIRA, C.; LOURENCO, J.; SOUSA, D.

Vydáno

18. 5. 2017

Nakladatel

Institute of Electrical and Electronics Engineers

Místo

Tokyo

ISBN

978-1-5090-6032-0

Kniha

2017 IEEE International Conference on Software Testing, Verification and Validation (ICST)

Strany od

196

Strany do

206

Strany počet

11

URL

https://www.fit.vut.cz/research/publication/11510/

BibTex

@inproceedings{BUT144470,
  author="Jan {Fiedor} and Tomáš {Vojnar} and Aleš {Smrčka} and Ricardo {Dias} and Carla {Ferreira} and Joao {Lourenco} and Diogo {Sousa}",
  title="Verifying Concurrent Programs Using Contracts",
  booktitle="2017 IEEE International Conference on Software Testing, Verification and Validation (ICST)",
  year="2017",
  pages="196--206",
  publisher="Institute of Electrical and Electronics Engineers",
  address="Tokyo",
  doi="10.1109/ICST.2017.25",
  isbn="978-1-5090-6032-0",
  url="https://www.fit.vut.cz/research/publication/11510/"
}