Write a Blog >>
Thu 23 Jan 2020 14:00 - 14:21 at Ile de France III (IDF III) - Abstract Interpretation Chair(s): Xavier Rival

In this paper we generalize the notion of extensional (functional) equivalence of programs to abstract equivalences induced by abstract interpretations. The standard notion of extensional equivalence is recovered as the special case, induced by the concrete interpretation. Some properties of the extensional equivalence, such as the one spelled out in Rice’s theorem, lift to the abstract equivalences in suitably generalized forms. On the other hand, the generalized framework gives rise to interesting and important new properties, and allows refined, non-extensional analyses. In particular, since programs turn out to be extensionally equivalent if and only if they are equivalent just for the concrete interpretation, it follows that any non-trivial abstract interpretation uncovers some intensional aspect of programs. This striking result is also effective, in the sense that it allows constructing, for any non-trivial abstraction, a pair of programs that are extensionally equivalent, but have different abstract semantics. The construction is based on the fact that abstract interpretations are always sound, but that they can be made incomplete through suitable code transformations. To construct these transformations, we introduce a novel technique for building incompleteness cliques of extensionally equivalent yet abstractly distinguishable programs: they are built together with abstract interpretations that produce false alarms. While programs are forced into incompleteness cliques using both control-flow and data-flow transformations, the main result follows from limitations of data-flow transformations with respect to control-flow ones. A further consequence is that the class of incomplete programs for a non-trivial abstraction is Turing complete. The obtained results also shed a new light on the relation between the techniques of code obfuscation and the precision in program analysis.

Abstract extensionality slides (POPL2020.pdf)13.94MiB

Thu 23 Jan

Displayed time zone: Saskatchewan, Central America change

14:00 - 15:05
Abstract InterpretationResearch Papers at Ile de France III (IDF III)
Chair(s): Xavier Rival INRIA/CNRS/ENS Paris
14:00
21m
Talk
Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations
Research Papers
Roberto Bruni University of Pisa, Roberto Giacobazzi University of Verona and IMDEA Software Institute, Roberta Gori University of Pisa, Isabel Garcia-Contreras IMDEA Software Institute, Dusko Pavlovic University of Hawaii
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Abstract Interpretation of Distributed Network Control Planes
Research Papers
Ryan Beckett Microsoft Research, Aarti Gupta Princeton University, Ratul Mahajan University of Washington, Intentionet, David Walker Princeton University
Link to publication DOI Media Attached File Attached
14:43
21m
Talk
Deterministic Parallel Fixpoint Computation
Research Papers
Sung Kook Kim University of California, Davis, Arnaud J. Venet Facebook, Aditya V. Thakur University of California, Davis
Link to publication DOI Pre-print Media Attached File Attached