Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1129347,
author = {Barnat, Jiří and Bauch, Petr and Havel, Vojtěch},
address = {Turin},
booktitle = {Proceedings of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP)},
doi = {http://dx.doi.org/10.1109/PDP.2014.44},
keywords = {ltl model checking; parallel programs; smt solvers},
howpublished = {elektronická verze "online"},
language = {eng},
location = {Turin},
pages = {756-759},
publisher = {IEEE Computer Society},
title = {Model Checking Parallel Programs with Inputs},
year = {2014}
}
TY - JOUR
ID - 1129347
AU - Barnat, Jiří - Bauch, Petr - Havel, Vojtěch
PY - 2014
TI - Model Checking Parallel Programs with Inputs
PB - IEEE Computer Society
CY - Turin
KW - ltl model checking
KW - parallel programs
KW - smt solvers
N2 - 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.
ER -
BARNAT, Jiří, Petr BAUCH and Vojtěch HAVEL. Model Checking Parallel Programs with Inputs. Online. In \textit{Proceedings of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP)}. Turin: IEEE Computer Society, 2014, p.~756-759. ISSN~1066-6192. Available from: https://dx.doi.org/10.1109/PDP.2014.44.
|
