NASA Logo, National Aeronautics and Space Administration

Probabilistic Program Analysis

Probabilistic software analysis aims at quantifying how likely a target event is to occur, given a probabilistic characterization of the behavior of a program or of its execution environment. Examples of target events may include an uncaught exception, the invocation of a certain method, or the access to confidential information.

We are working on a symbolic execution approach to probabilistic software analysis that first computes the conditions to reach the target event, and then tries to quantify the fraction of the input domain satisfying these conditions. Unlike past approaches, that were mostly performed at model level, and were thus only applicable to early software design stages or required explicit (and hard to maintain) abstraction from the code, our techniques are performed directly at the code level.

Our techniques are built on top of the Symbolic PathFinder symbolic execution tool. Applications range from program understanding and debugging to computing reliability of software operating in uncertain environments.


  • Reliability Analysis in Symbolic Pathfinder, Antonio Filieri, Corina S. Păsăreanu, and Willem Visser. In ICSE 2013.
  • Compositional Solution Space Quantification for Probabilistic Software Analysis. Mateus Borges, Federal University of Pernambuco; Antonio Filieri, University of Stuttgart; Marcelo D'Amorim, Federal University of Pernambuco; Corina S. Pasareanu, Carnegie Mellon Silicon Valley, NASA Ames; Willem Visser, Stellenbosch University. In PLDI 2014.
  • Statistical Symbolic Execution with Informed Sampling, Antonio Filieri, Corina S. Păsăreanu, Willem Visser, and Jaco Geldenhuys. In FSE 2014.
  • Exact and Approximate Probabilistic Symbolic Execution for Nondeterministic Programs, Kasper Luckow, Corina S. Pasareanu, Matt Dwyer, Antonio Filieri, Willem Visser. In ASE 2014.
  • Quantifying Information Leaks using Reliability Analysis, Quoc-Sang Phan, Pasquale Malacaria, Corina Pasareanu and Marcelo D'Amorim. In SPIN 2014 (short).


  • Antonio Filieri (University of Sttutgart, Germany)
  • Willem Visser and Jaco Geldenhuys (University of Stellenbosch, South Africa)
  • Kasper Luckow (Aalborg University, Denmark)
  • Matt Dwyer and Sebastain Elbaum (University of Nebraska, Lincoln, USA)
  • Marcelo d'Amorim and Mateus Borges (Federal University of Pernambuco, Brazil)

First Gov logo
NASA Logo -