D 2014

Model Checking Parallel Programs with Inputs

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

Basic information

Original name

Model Checking Parallel Programs with Inputs

Authors

BARNAT, Jiří (203 Czech Republic, belonging to the institution), Petr BAUCH (203 Czech Republic, belonging to the institution) and Vojtěch HAVEL (203 Czech Republic, belonging to the institution)

Edition

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

Publisher

IEEE Computer Society

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

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

Publication form

electronic version available online

RIV identification code

RIV/00216224:14330/14:00073421

Organization unit

Faculty of Informatics

ISSN

DOI

UT WoS

000353964700109

Keywords in English

ltl model checking; parallel programs; smt solvers

Tags

Tags

International impact, Reviewed
Změněno: 27/2/2018 06:59, RNDr. Pavel Šmerk, Ph.D.

Abstract

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.

Links

GAP202/11/0312, research and development project
Name: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Acronym: Components in Embedded Systems)
Investor: Czech Science Foundation
MUNI/A/0760/2012, interní kód MU
Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Acronym: FI MAV II.)
Investor: Masaryk University, Category A
MUNI/A/0765/2013, interní kód MU
Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Category A
MUNI/A/0855/2013, interní kód MU
Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Acronym: FI MAV III.)
Investor: Masaryk University, Category A