Model Checking Parallel Programs with Inputs

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BARNAT Jiří BAUCH Petr HAVEL Vojtěch

Year of publication 2014
Type Article in Proceedings
Conference Proceedings of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP)
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1109/PDP.2014.44
Field Informatics
Keywords ltl model checking; parallel programs; smt solvers
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.