Extended probabilistic symbolic execution

[摘要] ENGLISH ABSTRACT: Probabilistic symbolic execution is a new approach that extends the normal symbolicexecution with probability calculations. This approach combines symbolic execution andmodel counting to estimate the number of input values that would satisfy a given pathcondition, and thus is able to calculate the execution probability of a path. The focushas been on programs that manipulate primitive types such as linear integer arithmeticin object-oriented programming languages such as Java. In this thesis, we extend probabilisticsymbolic execution to handle data structures, thus allowing support for referencetypes. Two techniques are proposed to calculate the probability of an execution when theprograms have structures as inputs: an approximate approach that assumes probabilitiesfor certain choices stay fixed during the execution and an accurate technique basedon counting valid structures. We evaluate these approaches on an example of a BinarySearch Tree and compare it to the classic approach which only take symbolic values asinput.

[发布机构] Stellenbosch University