Verifying Concurrent Programs Using Contracts

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F17%3APU126447" target="_blank" >RIV/00216305:26230/17:PU126447 - isvavai.cz</a>

Výsledek na webu

<a href="http://www.fit.vutbr.cz/research/pubs/all.php?id=11510" target="_blank" >http://www.fit.vutbr.cz/research/pubs/all.php?id=11510</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1109/ICST.2017.25" target="_blank" >10.1109/ICST.2017.25</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Verifying Concurrent Programs Using Contracts

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Verifying Concurrent Programs Using Contracts

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

20206 - Computer hardware and architecture

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2017

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

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

ISBN

978-1-5090-6032-0

ISSN

—

e-ISSN

—

Počet stran výsledku

11

Strana od-do

196-206

Název nakladatele

Institute of Electrical and Electronics Engineers

Místo vydání

Tokyo

Místo konání akce

Tokyo

Datum konání akce

13. 2. 2017

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000403393600018