BARNAT, Jiří, Ivana ČERNÁ, Petr ROČKAI, Vladimír ŠTILL and Kristína ZÁKOPČANOVÁ. On verifying C++ programs with probabilities (On verifying {C++} programs with probabilities). In Sascha Ossowski. Proceedings of the 31st Annual ACM Symposium on Applied Computing. Pisa: ACM New York, NY, USA, 2016, p. 1238-1243. ISBN 978-1-4503-3739-7. Available from: https://dx.doi.org/10.1145/2851613.2851721.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name On verifying C++ programs with probabilities
Authors BARNAT, Jiří (203 Czech Republic, guarantor, belonging to the institution), Ivana ČERNÁ (203 Czech Republic, belonging to the institution), Petr ROČKAI (703 Slovakia, belonging to the institution), Vladimír ŠTILL (203 Czech Republic, belonging to the institution) and Kristína ZÁKOPČANOVÁ (203 Czech Republic, belonging to the institution).
Edition Pisa, Proceedings of the 31st Annual ACM Symposium on Applied Computing, p. 1238-1243, 6 pp. 2016.
Publisher ACM New York, NY, USA
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Italy
Confidentiality degree is not subject to a state or trade secret
Publication form storage medium (CD, DVD, flash disk)
WWW URL
RIV identification code RIV/00216224:14330/16:00088057
Organization unit Faculty of Informatics
ISBN 978-1-4503-3739-7
Doi http://dx.doi.org/10.1145/2851613.2851721
Keywords in English Model Checking; Probabilistic systems; DIVINE ; PRISM
Tags core_B, firank_A
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Ivana Černá, CSc., učo 1419. Changed: 16/7/2018 15:46.
Abstract
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.
Links
GA15-08772S, research and development projectName: Analýza korektnosti vícevláknových programů v C a C++
Investor: Czech Science Foundation
MUNI/A/0935/2015, interní kód MUName: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Category A
MUNI/A/0945/2015, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.
Investor: Masaryk University, Category A
PrintDisplayed: 25/9/2024 10:10