Algorithmic advances in data-flow and quantitative analysis

By Andreas Pavlogiannis

Abstract
Static analysis is a standard approach for program verification and optimization. The talk will introduce some new techniques for data-flow and quantitative analysis, and is structured in two parts.

In the first part, I will present the Quantitative Interprocedural Analysis (QIA) framework. I will illustrate how several quantitative problems related to static analysis of recursive programs can be cast as QIA instances. I will sketch the algorithmic approach to performing QIA, and present some case studies.

In the second part, I will focus on exploiting the graph-theoretic notion of treewidth for program analysis. I will present recent algorithmic advances in data-flow and quantitative analysis of procedural and concurrent programs, which exploit the fact that control-flow graphs are typically graphs of small treewidth. Besides improved complexity bounds, the new approaches are suitable for on-demand analysis with strong complexity guarantees.

Bio
Andreas Pavlogiannis is a Ph.D. candidate at the Institute of Science and Technology Austria, working on algorithmic aspects of formal verification. He obtained a Master's degree from the University of California at Davis, and a Bachelor's degree from the University of Patras in Greece.

More information