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.


  • 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 -