Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{1350754, author = {Barnat, Jiří and Černá, Ivana and Ročkai, Petr and Štill, Vladimír and Zákopčanová, Kristína}, address = {Pisa}, booktitle = {Proceedings of the 31st Annual ACM Symposium on Applied Computing}, doi = {http://dx.doi.org/10.1145/2851613.2851721}, editor = {Sascha Ossowski}, keywords = {Model Checking; Probabilistic systems; DIVINE ; PRISM}, howpublished = {paměťový nosič}, language = {eng}, location = {Pisa}, isbn = {978-1-4503-3739-7}, pages = {1238-1243}, publisher = {ACM New York, NY, USA}, title = {On verifying C++ programs with probabilities}, url = {http://doi.acm.org/10.1145/2851613.2851721}, year = {2016} }
TY - JOUR ID - 1350754 AU - Barnat, Jiří - Černá, Ivana - Ročkai, Petr - Štill, Vladimír - Zákopčanová, Kristína PY - 2016 TI - On verifying C++ programs with probabilities PB - ACM New York, NY, USA CY - Pisa SN - 9781450337397 KW - Model Checking KW - Probabilistic systems KW - DIVINE KW - PRISM UR - http://doi.acm.org/10.1145/2851613.2851721 N2 - 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. ER -
BARNAT, Jiří, Ivana ČERNÁ, Petr ROČKAI, Vladimír ŠTILL a Kristína ZÁKOPČANOVÁ. On verifying C++ programs with probabilities. In Sascha Ossowski. \textit{Proceedings of the 31st Annual ACM Symposium on Applied Computing}. Pisa: ACM New York, NY, USA, 2016, s.~1238-1243. ISBN~978-1-4503-3739-7. Dostupné z: https://dx.doi.org/10.1145/2851613.2851721.
|