Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS seminar: Antonio Filieri: Probabilistic Symbolic Execution: Bringing quantitative analysis at code level

LFCS seminar: Antonio Filieri: Probabilistic Symbolic Execution: Bringing quantitative analysis at code level

— filed under:

What
  • LFCS Seminar
When Mar 15, 2016
from 04:00 PM to 05:00 PM
Where IF 4.31/4.33
Add event to calendar vCal
iCal

[Title]

Probabilistic Symbolic Execution: Bringing quantitative analysis at code level

[Abstract]

(tentative)

Quantitative verification is taking on a critical importance on software design and evaluation. Engineers extract a variety of abstract formal models of software behaviors and analyze them via probabilistic model checking or numerical methods. However, while extracting quantitative formal views from design models is a consolidated practice, keeping them synchronized 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 reaching a desired target state. PSE combines symbolic execution with model counting and solution space quantification techniques to automatically abstract and quantitatively analyze 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.

[Short bio]

 

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 .

Document Actions