Model Checking Parallel Programs with Inputs

• Autoři: BARNAT Jiří; BAUCH Petr; HAVEL Vojtěch
• Rok publikování: 2014
• Druh: Článek ve sborníku
• Konference: Proceedings of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP)
• Fakulta / Pracoviště MU: Fakulta informatiky
• Doi: http://dx.doi.org/10.1109/PDP.2014.44
• Obor: Informatika
• Klíčová slova: ltl model checking; parallel programs; smt solvers
• Popis: 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.

Související projekty

• Software Components in Embedded Systems: Development and Verification
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II.
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III.
• Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity