Scalable Program Analysis via Decompositions of Control-flow Graphs
- Day - Time: 09 December 2025, h.11:00
- Place: Area della Ricerca CNR di Pisa - Room: Faedo
Speakers
- Amir K. Goharshady (Department of Computer Science, University of Oxford)
Referent
Abstract
Many classical tasks in formal verification, compiler optimization, and program analysis 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 represent the sparsity of graphs arising in programs in terms of treewidth, pathwidth and SPL (series-parallel-loop) decompositions and offer new bounds and algorithms that scale lightweight formal methods to millions of lines of code.