Algorithmic Advances in Automated Program Analysis
Event details
| Date | 22.01.2019 |
| Hour | 10:00 › 11:00 |
| Speaker | Andreas Pavlogiannis |
| Location | |
| Category | Conferences - Seminars |
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 of concurrent programs. I will outline some foundational limitations to existing DPOR algorithms, and then present some recent efforts in overcoming these limitations in a fundamental way. I will conclude with an outlook on current challenges and future directions.
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.
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 of concurrent programs. I will outline some foundational limitations to existing DPOR algorithms, and then present some recent efforts in overcoming these limitations in a fundamental way. I will conclude with an outlook on current challenges and future directions.
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.
Practical information
- General public
- Free
Contact
- EDIC - [email protected]