D 2014

Model Checking Parallel Programs with Inputs

BARNAT, Jiří, Petr BAUCH a Vojtěch HAVEL

Základní údaje

Originální název

Model Checking Parallel Programs with Inputs

Autoři

BARNAT, Jiří (203 Česká republika, domácí), Petr BAUCH (203 Česká republika, domácí) a Vojtěch HAVEL (203 Česká republika, domácí)

Vydání

Turin, Proceedings of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP), od s. 756-759, 4 s. 2014

Nakladatel

IEEE Computer Society

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Kód RIV

RIV/00216224:14330/14:00073421

Organizační jednotka

Fakulta informatiky

ISSN

DOI

UT WoS

000353964700109

Klíčová slova anglicky

ltl model checking; parallel programs; smt solvers

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 27. 2. 2018 06:59, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Verification of parallel programs with input variables represents a significant and well-motivated challenge. This paper addresses the challenge with a verification method that combines explicit and symbolic approaches to the state space representation. The state matching between non-canonical representations proved to be the bottleneck of such a combination, since its computation entailed deciding satisfiability of quantified bit-vector formulae. This limitation is here addressed by an alternative state matching, based on quantifier-free, and a heuristics optimising the state space searching. The experimental evaluation shows that the alternative state matching causes only a minor increase in the number of states and that, in combination with the heuristics, it considerably extends the scope of applicability of the proposed LTL model checking.

Návaznosti

GAP202/11/0312, projekt VaV
Název: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems)
Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification
MUNI/A/0760/2012, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Akronym: FI MAV II.)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0765/2013, interní kód MU
Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0855/2013, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Akronym: FI MAV III.)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty