Thesis (MSc)--Stellenbosch University, 2013. / ENGLISH ABSTRACT: Probabilistic symbolic execution is a new approach that extends the normal symbolic
execution with probability calculations. This approach combines symbolic execution and
model counting to estimate the number of input values that would satisfy a given path
condition, and thus is able to calculate the execution probability of a path. The focus
has been on programs that manipulate primitive types such as linear integer arithmetic
in object-oriented programming languages such as Java. In this thesis, we extend probabilistic
symbolic execution to handle data structures, thus allowing support for reference
types. Two techniques are proposed to calculate the probability of an execution when the
programs have structures as inputs: an approximate approach that assumes probabilities
for certain choices stay fixed during the execution and an accurate technique based
on counting valid structures. We evaluate these approaches on an example of a Binary
Search Tree and compare it to the classic approach which only take symbolic values as
input. / AFRIKAANSE OPSOMMING: Probabilistiese simboliese uitvoering is ’n nuwe benadering wat die normale simboliese
uitvoering uitbrei deur waarksynlikheidsberekeninge by te voeg. Hierdie benadering kombineer
simboliese uitvoering en modeltellings om die aantal invoerwaardes wat ’n gegewe
padvoorwaarde sal bevredig, te beraam en is dus in staat om die uitvoeringswaarskynlikheid
van ’n pad te bereken. Tot dus vêr was die fokus op programme wat primitiewe
datatipes manipuleer, byvoorbeeld lineêre heelgetalrekenkunde in objek-geörienteerde tale
soos Java. In hierdie tesis brei ons probabilistiese simboliese uitvoering uit om datastrukture,
en dus verwysingstipes, te dek. Twee tegnieke word voorgestel om die uitvoeringswaarskynlikheid
van ’n program met datastrukture as invoer te bereken. Eerstens is daar
die benaderingstegniek wat aanneem dat waarskynlikhede vir sekere keuses onveranderd
sal bly tydens die uitvoering van die program. Tweedens is daar die akkurate tegniek wat
gebaseer is op die telling van geldige datastrukture. Ons evalueer hierdie benaderings op
’n voorbeeld van ’n binêre soekboom en vergelyk dit met die klassieke tegniek wat slegs
simboliese waardes as invoer neem.
| Identifer | oai:union.ndltd.org:netd.ac.za/oai:union.ndltd.org:sun/oai:scholar.sun.ac.za:10019.1/85804 |
| Date | 12 1900 |
| Creators | Uwimbabazi, Aline |
| Contributors | Visser, Willem, Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. |
| Publisher | Stellenbosch : Stellenbosch University |
| Source Sets | South African National ETD Portal |
| Language | en_ZA |
| Detected Language | English |
| Type | Thesis |
| Format | 70 p. : ill. |
| Rights | Stellenbosch University |
Page generated in 0.0024 seconds