POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

This program is tentative and subject to change.

Wed 22 Jan 2025 11:20 - 11:40 at Peek-A-Boo - Program Analysis

We study “the best of abstract interpretations”, namely, the best possible abstract interpretations of programs. Abstract interpretations of programs on a given abstract domain A are inductively defined by composing abstract transfer functions for the basic commands, such as assignments and Boolean guards. However, abstract interpretation is not compositional: even if the abstract transfer functions of the basic commands are the best possible in A this does not imply that the whole inductive abstract interpretation of a program P is still the best in A. When this happens we are in the optimal scenario where the abstract interpretation of P coincides with the abstraction of the concrete interpretation of P. Our main contributions are threefold. Firstly, we investigate the computability properties of the class of programs having the best possible abstract interpretation on a fixed abstract domain A. We show that this class is, in general, not straightforward and not recursive. We also prove the impossibility of achieving the best possible abstract interpretation of any program by an effective compilation. Secondly, we show that given an abstract interpretation of a program P on an abstract domain A, this domain cannot be minimally refined or simplified to attain the best possible abstract interpretation of P. These results show that the program property of having the best possible abstract interpretation is not trivial and, in general, hard to achieve. We then show how to prove that the abstract interpretation of a program is indeed the best possible one. This is achieved using a program logic parameterized on A which infers triples [pre]_A P [post]_A. These triples encode that the inductive abstract interpretation of P on A with abstract input pre ∈ A gives post ∈ A as abstract output and this is the best possible in A.

This program is tentative and subject to change.

Wed 22 Jan

Displayed time zone: Mountain Time (US & Canada) change

10:40 - 12:00
Program AnalysisPOPL at Peek-A-Boo
10:40
20m
Talk
Maximal Simplification of Polyhedral Reductions
POPL
Louis Narmour Colorado State University, Tomofumi Yuki , Sanjay Rajopadhye Colorado State University
11:00
20m
Talk
Program Analysis via Multiple Context Free Language Reachability
POPL
Giovanna Kobus Conrado Hong Kong University of Science and Technology, Adam Husted Kjelstrøm Aarhus University, Jaco van de Pol Aarhus University, Andreas Pavlogiannis Aarhus University
11:20
20m
Talk
The Best of Abstract Interpretations
POPL
Roberto Giacobazzi University of Arizona, Francesco Ranzato Dipartimento di Matematica, University of Padova, Italy
11:40
20m
Talk
An Incremental Algorithm for Algebraic Program Analysis
POPL
Chenyu Zhou University of Southern California, Yuzhou Fang University of Southern California, Jingbo Wang Purdue University, Chao Wang University of Southern California