On verifying C++ programs with probabilities

D 2016

On verifying C++ programs with probabilities

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

Základní údaje

Originální název

On verifying C++ programs with probabilities

Autoři

BARNAT, Jiří (203 Česká republika, garant, domácí), Ivana ČERNÁ (203 Česká republika, domácí), Petr ROČKAI (703 Slovensko, domácí), Vladimír ŠTILL (203 Česká republika, domácí) a Kristína ZÁKOPČANOVÁ (203 Česká republika, domácí)

Vydání

Pisa, Proceedings of the 31st Annual ACM Symposium on Applied Computing, od s. 1238-1243, 6 s. 2016

Nakladatel

ACM New York, NY, USA

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Itálie

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

paměťový nosič (CD, DVD, flash disk)

Odkazy

URL

Kód RIV

RIV/00216224:14330/16:00088057

Organizační jednotka

Fakulta informatiky

ISBN

978-1-4503-3739-7

DOI

http://dx.doi.org/10.1145/2851613.2851721

Klíčová slova anglicky

Model Checking; Probabilistic systems; DIVINE ; PRISM

Štítky

core_B, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 16. 7. 2018 15:46, prof. RNDr. Ivana Černá, CSc.

Anotace

V originále

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.

Návaznosti

GA15-08772S, projekt VaV

Název: Analýza korektnosti vícevláknových programů v C a C++

Investor: Grantová agentura ČR, Correctness Analysis of C and C++ Programs with Threads

MUNI/A/0935/2015, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

MUNI/A/0945/2015, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

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. 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.

@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.

Podrobný výpis o publikaci