A Journey into the (In)Completeness of Program Analysis by Abstract Interpretation

Tuesday, February 10, 2026
Schedule : 11:00
Marco Campion (APR, LIP6, Sorbonne Université)

Static program analysis aims at automatically reasoning about the behavior of programs, with the goal of detecting bugs or proving the absence of certain runtime errors. A fundamental challenge in this setting is the unavoidable trade-off between precision and decidability: the more expressive the property we want to analyze, the harder it becomes to compute it exactly. Abstract interpretation, introduced by Patrick and Radhia Cousot in 1977, provides a unifying mathematical framework to address this challenge by construction. Its key idea is to approximate program semantics in a sound way, ensuring that no real behaviors are missed, at the price of possibly introducing spurious ones. In this talk, I will first introduce the basic principles of program analysis by abstract interpretation, with an emphasis on intuition rather than technical details. I will then focus on the notion of completeness, which informally corresponds to the absence of false alarms. While completeness is a highly desirable property, it is in most cases impossible to achieve, as it would require solving undecidable problems exactly. The key takeaway of this talk is that, instead of striving for full completeness, a more realistic goal is to understand and characterize how and to what extent an analysis is incomplete. In this perspective, I will present the notion of partial completeness, which allows one to formally reason about controlled and limited forms of incompleteness in abstract interpretation.

Salle 428, couloir 26-00, 4 place Jussieu - 75005 Paris