| Title | Symbolic execution and probabilistic reasoning |
| Publication Type | Conference Paper |
| Year of Publication | 2017 |
| Authors | Pasareanu, C. |
| Conference Name | 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
| Date Published | jun |
| Keywords | Atmospheric modeling, Cognition, Computational modeling, Computing Theory, event occurrence probability, inference mechanisms, Metrics, Probabilistic logic, probabilistic reasoning, probability, program behaviors, program diagnostics, program paths, pubcrawl, reliability theory, safety-critical software, security metrics, software system safety, software system security, Software systems, symbolic execution, symbolic path conditions, systematic program analysis technique, Systematics |
| Abstract | Summary form only given. Symbolic execution is a systematic program analysis technique which explores multiple program behaviors all at once by collecting and solving symbolic path conditions over program paths. The technique has been recently extended with probabilistic reasoning. This approach computes the conditions to reach target program events of interest and uses model counting to quantify the fraction of the input domain satisfying these conditions thus computing the probability of event occurrence. This probabilistic information can be used for example to compute the reliability of an aircraft controller under different wind conditions (modeled probabilistically) or to quantify the leakage of sensitive data in a software system, using information theory metrics such as Shannon entropy. In this talk we review recent advances in symbolic execution and probabilistic reasoning and we discuss how they can be used to ensure the safety and security of software systems. |
| DOI | 10.1109/LICS.2017.8005062 |
| Citation Key | pasareanu_symbolic_2017 |
Symbolic execution and probabilistic reasoning