Special Seminar: Andreas Pavlogiannis "Algorithmic Advances in Automated Program Analysis"

Algorithmic Advances in Automated Program Analysis

Andreas Pavlogiannis

Abstract:

Modern-day software is increasingly complex and software engineering is commonly accepted as a challenging, error-prone task. Consequently, software bugs are prevalent, incurring detrimental financial costs and often risking human lives. Program analyses provide rigorous and effective means to automated bug detection, and are becoming an integral part of the software development process. In this talk, I will present recent algorithmic advances in two impactful domains of program analysis: (i) static analysis and (ii) stateless model checking.

Static analyses are lightweight approximations to program behavior and largely constitute the first step to bug detection in the software development process. In the first part, I will introduce the Algebraic Path Problem on Recursive Graphs (APP) and its close variant of Dyck Reachability (DR). These problems serve as algorithmic formulations of static analyses on various domains, such as dataflow/alias/data-dependence analysis and program slicing. I will present new algorithms for APP and DR based on the graph-theoretic notion of treewidth, that lead to theoretical complexity improvements and provide a significant scalability boost in practice. I will also introduce quantitative extensions to APP that can assist with code optimization at compilation time.

Stateless model checking is one of the most influential techniques in the analysis of concurrent programs because of its effectiveness in dealing with the state-explosion problem. In the second part, I will present Dynamic Partial Order Reduction (DPOR), a widespread stateless technique for model checking concurrent programs. I will outline some foundational limitations to existing DPOR approaches, and introduce a new abstraction of concurrent semantics, called the Observation Equivalence (OE), which overcomes some of these limitations. I will demonstrate algorithmic applications of OE in two domains: (i) stateless model checking and (ii) dynamic race detection.

Bio:

Andreas Pavlogiannis is a postdoctoral researcher in the Lab for Automated Reasoning and Analysis at Ecole Polytechnique Federale de Lausanne (EPFL) in Switzerland. His research focuses on algorithmic aspects of programming languages and software verification. He develops algorithms -- based on rigorous foundations such as automata theory, graph theory and combinatorial optimization -- which reason about program correctness and can also assist the compiler towards performance optimizations. Andreas's current research is supported by a Schrodinger Fellowship as well as an INRIA-EPFL Fellowship. He received a doctoral degree in computer science from the Institute of Science and Technology (IST) Austria. Prior to that, he received a master's degree in computer science from the University of California, Davis, and a joint bachelor-master's degree in computer engineering from the University of Patras in Greece.