This program is tentative and subject to change.
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 JanDisplayed time zone: Mountain Time (US & Canada) change
10:40 - 12:00 | |||
10:40 20mTalk | Maximal Simplification of Polyhedral Reductions POPL Louis Narmour Colorado State University, Tomofumi Yuki , Sanjay Rajopadhye Colorado State University | ||
11:00 20mTalk | 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 20mTalk | The Best of Abstract Interpretations POPL Roberto Giacobazzi University of Arizona, Francesco Ranzato Dipartimento di Matematica, University of Padova, Italy | ||
11:40 20mTalk | 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 |