In this paper, we report on successful chaining of two unique model checkers, namely DIVINE and PRISM, which, as a whole, allows for practical verification of multi-threaded C++ programs that may choose input and other actions according to a given discrete probabilistic distribution. In the paper, we discuss technical details of the extensions of the DIVINE model checker that were required to enable the chaining, in particular, we report on combination of dynamic τ+reduction used within the DIVINE state space exploration engine with the probabilistic choice operator. We also give preliminary experimental evaluation of our approach, discuss some possible applications for the tool chain, and finally, we plot some of the future steps to be done.
['Jiří Barnat', 'Ivana Černá', 'Petr Ročkai', 'Vladimír Štill', 'Kristína Zákopčanová']
On verifying C++ programs with probabilities