Probabilistic Symbolic Execution: Moving quantitative analysis from models to code

Quantitative verification is taking on a critical importance on software design and evaluation.  Engineers extract a variety of abstract formal models of software behaviours and analyse them via probabilistic model checking or numerical methods.  However, while extracting quantitative formal views from design models is a consolidated practice, keeping them synchronised with the actual implementation is a much harder problem.  In turn, most applications of quantitative verification are either limited to the early stages of the process or require a significant effort to keep the models updated.

Probabilistic Symbolic Execution (PSE) is a static program analysis technique for computing the probability a software execution will follow a specific path or will reach a desired target state.  PSE combines symbolic execution with model counting and solution space quantification techniques to automatically abstract and quantitatively analyse code artifacts.  Furthermore, the analysis can be tailored to specific usage profiles and used to solve some classes of synthesis problems automatically.

In this talk, I will overview the main results on PSE and discuss the main open challenges for its further development.

Speaker biography

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.  More info at www.antonio.filieri.name.