Static Analyses for the Properties, Programs, and People of Tomorrow

Caterina Urban

Abstract

This documents presents an overview of my research journey aimed at enhancing the quality and reliability of modern software systems through advanced static analyses. Rooted in the theory of abstract interpretation, my work broadens the scope of static program analysis to address a diverse range of functional properties, hyperproperties, and quantitative properties. Through a blend of theoretical contributions and practical tool development, my research contributes static analysis methods for verifying temporal logic specifications, detecting vulnerable variables in adversarial settings, as well as quantifying analysis imprecision and comparing static analyses. It also pioneers static analyses tailored to new audiences – such as data scientists – and software domains – such as machine learning development pipelines. The overarching vision is to make static analysis more expressive, accessible, and aligned with the evolving needs of software, its developers, and its users.