Probabilistic symbolic execution: a bird's eye view

Probabilistic symbolic execution is a static program analysis technique for computing probabilistic measures over the space of execution paths of a program, optionally conditioned on specific usage profiles. In its basic formulation, it aims at computing the probability of a program reaching specific target states during the execution, e.g., invoking a specific function or throwing an exception. More recent applications include quantitative security analysis, program similarity, and code level performance analysis. This talk will overview some of the main principles and challenges behind the working of probabilistic symbolic execution, and discuss a set of its current and envisioned applications.

Antonio Filieri is a Lecturer (Assistant Professor) at Imperial College London.  His main research interests are in the application of mathematical methods to software engineering, in particular probability, statistics, logic, and control theory.  The main topics of his recent publications include exact and approximate analysis methods for probabilistic software analysis, control-theoretical software adaptation, quantitative software modeling and verification at runtime, and incremental verification.  

https://antonio.filieri.name