Exact and approximate probabilistic symbolic execution for nondeterministic programs

Kasper Søe Luckow; Corina S. Păsăreanu; Matthew B. Dwyer; Antonio Filieri; Willem Visser

doi:10.1145/2642937.2643011

Exact and approximate probabilistic symbolic execution for nondeterministic programs

Kasper Søe Luckow, Corina S. Păsăreanu, Matthew B. Dwyer, Antonio Filieri, Willem Visser

Department of Computer Science

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

36 Citations (Scopus)

Abstract

Probabilistic software analysis seeks to quantify the likelihood of reaching a target event under uncertain environments. Recent approaches compute probabilities of execution paths using symbolic execution, but do not support nondeterminism. Nondeterminism arises naturally when no suitable probabilistic model can capture a program behavior, e.g., for multithreading or distributed systems.

In this work, we propose a technique, based on symbolic execution, to synthesize schedulers that resolve nondeterminism to maximize the probability of reaching a target event. To scale to large systems, we also introduce approximate algorithms to search for good schedulers, speeding up established random sampling and reinforcement learning results through the quantification of path probabilities based on symbolic execution.

We implemented the techniques in Symbolic PathFinder and evaluated them on nondeterministic Java programs. We show that our algorithms significantly improve upon a state-of-the-art statistical model checking algorithm, originally developed for Markov Decision Processes.

Original language	English
Title of host publication	Proceedings of the 29th ACM/IEEE international conference on Automated software engineering
Publisher	Association for Computing Machinery
Publication date	2014
Pages	575-586
ISBN (Print)	978-1-4503-3013-8
DOIs	https://doi.org/10.1145/2642937.2643011
Publication status	Published - 2014
Event	The 29th ACM/IEEE International Conference on Automated Software Engineering - Aros Congress Center, Västerås, Sweden Duration: 15 Sept 2014 → 19 Sept 2014 Conference number: 29

Conference

Conference	The 29th ACM/IEEE International Conference on Automated Software Engineering
Number	29
Location	Aros Congress Center
Country/Territory	Sweden
City	Västerås
Period	15/09/2014 → 19/09/2014

Series	Automated Software Engineering
ISSN	0928-8910

Access to Document

10.1145/2642937.2643011

AUB Link

Search for the material in Aalborg University Library's search engine

36 Citations
1 PhD thesis

Platforms and Model-Based Analyses for Real-Time Java
Luckow, K. S., 2014, Department of Computer Science, Aalborg University.
Research output: PhD thesis

Cite this

@inproceedings{c120c9b8a04c43b28ef10bb9d376e81d,

title = "Exact and approximate probabilistic symbolic execution for nondeterministic programs",

abstract = "Probabilistic software analysis seeks to quantify the likelihood of reaching a target event under uncertain environments. Recent approaches compute probabilities of execution paths using symbolic execution, but do not support nondeterminism. Nondeterminism arises naturally when no suitable probabilistic model can capture a program behavior, e.g., for multithreading or distributed systems.In this work, we propose a technique, based on symbolic execution, to synthesize schedulers that resolve nondeterminism to maximize the probability of reaching a target event. To scale to large systems, we also introduce approximate algorithms to search for good schedulers, speeding up established random sampling and reinforcement learning results through the quantification of path probabilities based on symbolic execution.We implemented the techniques in Symbolic PathFinder and evaluated them on nondeterministic Java programs. We show that our algorithms significantly improve upon a state-of-the-art statistical model checking algorithm, originally developed for Markov Decision Processes.",

author = "Luckow, {Kasper S{\o}e} and P{\u a}s{\u a}reanu, {Corina S.} and Dwyer, {Matthew B.} and Antonio Filieri and Willem Visser",

year = "2014",

doi = "10.1145/2642937.2643011",

language = "English",

isbn = "978-1-4503-3013-8",

series = "Automated Software Engineering",

publisher = "Association for Computing Machinery",

pages = "575--586",

booktitle = "Proceedings of the 29th ACM/IEEE international conference on Automated software engineering",

address = "United States",

note = "The 29th ACM/IEEE International Conference on Automated Software Engineering ; Conference date: 15-09-2014 Through 19-09-2014",

}

Luckow, KS, Păsăreanu, CS, Dwyer, MB, Filieri, A & Visser, W 2014, Exact and approximate probabilistic symbolic execution for nondeterministic programs. in Proceedings of the 29th ACM/IEEE international conference on Automated software engineering. Association for Computing Machinery, Automated Software Engineering, pp. 575-586, The 29th ACM/IEEE International Conference on Automated Software Engineering, Västerås, Sweden, 15/09/2014. https://doi.org/10.1145/2642937.2643011

Exact and approximate probabilistic symbolic execution for nondeterministic programs. / Luckow, Kasper Søe; Păsăreanu, Corina S.; Dwyer, Matthew B. et al.
Proceedings of the 29th ACM/IEEE international conference on Automated software engineering. Association for Computing Machinery, 2014. p. 575-586 (Automated Software Engineering).

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

TY - GEN

T1 - Exact and approximate probabilistic symbolic execution for nondeterministic programs

AU - Luckow, Kasper Søe

AU - Păsăreanu, Corina S.

AU - Dwyer, Matthew B.

AU - Filieri, Antonio

AU - Visser, Willem

N1 - Conference code: 29

PY - 2014

Y1 - 2014

N2 - Probabilistic software analysis seeks to quantify the likelihood of reaching a target event under uncertain environments. Recent approaches compute probabilities of execution paths using symbolic execution, but do not support nondeterminism. Nondeterminism arises naturally when no suitable probabilistic model can capture a program behavior, e.g., for multithreading or distributed systems.In this work, we propose a technique, based on symbolic execution, to synthesize schedulers that resolve nondeterminism to maximize the probability of reaching a target event. To scale to large systems, we also introduce approximate algorithms to search for good schedulers, speeding up established random sampling and reinforcement learning results through the quantification of path probabilities based on symbolic execution.We implemented the techniques in Symbolic PathFinder and evaluated them on nondeterministic Java programs. We show that our algorithms significantly improve upon a state-of-the-art statistical model checking algorithm, originally developed for Markov Decision Processes.

AB - Probabilistic software analysis seeks to quantify the likelihood of reaching a target event under uncertain environments. Recent approaches compute probabilities of execution paths using symbolic execution, but do not support nondeterminism. Nondeterminism arises naturally when no suitable probabilistic model can capture a program behavior, e.g., for multithreading or distributed systems.In this work, we propose a technique, based on symbolic execution, to synthesize schedulers that resolve nondeterminism to maximize the probability of reaching a target event. To scale to large systems, we also introduce approximate algorithms to search for good schedulers, speeding up established random sampling and reinforcement learning results through the quantification of path probabilities based on symbolic execution.We implemented the techniques in Symbolic PathFinder and evaluated them on nondeterministic Java programs. We show that our algorithms significantly improve upon a state-of-the-art statistical model checking algorithm, originally developed for Markov Decision Processes.

U2 - 10.1145/2642937.2643011

DO - 10.1145/2642937.2643011

M3 - Article in proceeding

SN - 978-1-4503-3013-8

T3 - Automated Software Engineering

SP - 575

EP - 586

BT - Proceedings of the 29th ACM/IEEE international conference on Automated software engineering

PB - Association for Computing Machinery

T2 - The 29th ACM/IEEE International Conference on Automated Software Engineering

Y2 - 15 September 2014 through 19 September 2014

ER -

Exact and approximate probabilistic symbolic execution for nondeterministic programs

Abstract

Conference

Access to Document

AUB Link

Research output

Platforms and Model-Based Analyses for Real-Time Java

Cite this