Probabilistic Programming for Java']Java using Symbolic Execution and Model Counting

被引：4

作者：

Visser, Willem ^{[1
]}

Pasareanu, Corina S. ^{[2
,3
]}

机构：

[1] Stellenbosch Univ, Stellenbosch, South Africa

[2] CMU West, Mountain View, CA USA

[3] NASA, Ames Res Ctr, Mountain View, CA USA

来源：

SOUTH AFRICAN INSTITUTE OF COMPUTER SCIENTISTS AND INFORMATION TECHNOLOGISTS (SACSIT 2017) | 2017年

关键词：

Probabilistic Programming; Symbolic Execution; Model Counting;

D O I：

10.1145/3129416.3129433

中图分类号：

TP39 [计算机的应用];

学科分类号：

081203 ; 0835 ;

摘要：

In this paper we describe a probabilistic programming environment for Java that is based on symbolic execution and model counting. The novelty of the framework is that the probability distributions in the program can themselves be symbolic, which allows parametric probabilistic programming. The framework handles typical probabilistic programming features, such as observe statements, and can be used for the encoding and analysis of Discrete Time Markov Chains (DTMC), Bayesian Networks, etc. We show two examples of using the system: (1) analysis of bubble sort when using an unreliable comparison operation, and, (2) analysis of a simulation model of autonomous aircraft towing vehicles, to show whether plans generated for these vehicles are robust when probability distributions are changed from the ones used to generate the plans.

引用

页码：319 / 328

页数：10

共 24 条

[1]

[Anonymous], 2014, PROC FOSE 14, DOI DOI 10.1145/2593882.2593900

[2] Automata-Based Model Counting for String Constraints [J].

Aydin, Abdulbaki ;

Bang, Lucas ;

Bultan, Tevfik .

COMPUTER AIDED VERIFICATION, PT I, 2015, 9206 :255-272

[3]

Borges M, 2014, ACM SIGPLAN NOTICES, V49, P123, DOI [10.1145/2594291.2594329, 10.1145/2666356.2594329]

[4] Symbolic Execution for Software Testing: Three Decades Later [J].

Cadar, Cristian ;

Sen, Koushik .

COMMUNICATIONS OF THE ACM, 2013, 56 (02) :82-90

[5]

DAWS C, 2005, THEOR ASP COMP, V3407, P280

[6]

De Moura Leonardo, 2008, P 14 INT C TOOLS ALG

[7] Model Counting for Complex Data Structures [J].

Filieri, Antonio ;

Frias, Marcelo F. ;

Pasareanu, Corina S. ;

Visser, Willem .

MODEL CHECKING SOFTWARE, SPIN 2015, 2015, 9232 :222-241

[8]

Filieri A, 2013, PROCEEDINGS OF THE 35TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE 2013), P622, DOI 10.1109/ICSE.2013.6606608

[9]

Geldenhuys Jaco, 2012, P ISSTA, P166, DOI [10.1145/2338965.2336773, DOI 10.1145/2338965.2336773]

[10] Probabilistic reachability for parametric markov models [J].

Hahn E.M. ;

Hermanns H. ;

Zhang L. .

International Journal on Software Tools for Technology Transfer, 2011, 13 (1) :3-19

← 1 2 3 →