Parameterized Algorithms for Scalable Program Analysis

Parameterized Algorithms for Scalable Program Analysis

Many classical tasks in compiler optimization, program analysis and formal verification are formalized in terms of graph problems, usually over the control-flow or call graphs of programs. Examples include data-flow analyses (such as null-pointer and reaching definitions), register allocation, and the entire framework of algebraic program analysis (APA). The resulting graph problems often end up being NP-hard. Even when a PTIME solution exists, it is not usually linear-time and fails to scale up to handle modern software systems with hundreds of millions of lines of code. 

As it turns out, control-flow and call graphs of programs are often sparse and exhibit certain desirable structures, such as tree-likeness, which can be exploited to obtain much faster algorithms for these classical tasks. In this talk, we formalize the sparsity of graphs arising in programs in terms of treewidth, pathwidth and SPL (series-parallel-loop) decompositions and present new bounds and algorithms that scale lightweight formal methods to millions of lines of code.

Amir Goharshady is an Assistant Professor of Computer Science and Mathematics at the Hong Kong University of Science and Technology. His research is focused theoretical computer science and spans formal methods, program verification, parameterized algorithms and blockchain technologies. 

See https://amir.goharshady.com/ for more information.