On verifying C++ programs with probabilities

Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

BARNAT Jiří ČERNÁ Ivana ROČKAI Petr ŠTILL Vladimír ZÁKOPČANOVÁ Kristína

Rok publikování 2016
Druh Článek ve sborníku
Konference Proceedings of the 31st Annual ACM Symposium on Applied Computing
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www http://doi.acm.org/10.1145/2851613.2851721
Doi http://dx.doi.org/10.1145/2851613.2851721
Obor Informatika
Klíčová slova Model Checking; Probabilistic systems; DIVINE ; PRISM
Popis In this paper, we report on successful chaining of two unique model checkers, namely DIVINE and PRISM, which, as a whole, allows for practical veri cation 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 ap- proach, discuss some possible applications for the tool chain, and nally, we plot some of the future steps to be done.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.