Write a Blog >>
Sun 20 - Fri 25 October 2019 Athens, Greece
Wed 23 Oct 2019 11:22 - 11:45 at Attica - Abstract Interpretation Chair(s): John Hughes

It is well known that a staged interpreter is a compiler: specializing an interpreter to a given program produces an equivalent executable that runs faster. This connection is known as the first Futamura projection. It is even more widely known that an abstract interpreter is a program analyzer: tweaking an interpreter to run on abstract domains produces a sound static analysis. What happens when we combine these two ideas, and apply specialization to an abstract interpreter?

In this paper, we present a unifying framework that naturally extends the first Futamura projection from concrete interpreters to abstract interpreters. Our approach derives a sound staged abstract interpreter based on a generic interpreter with type-level binding-time abstractions and monadic abstractions. By using different instantiations of these abstractions, the generic interpreter can flexibly behave in one of four modes: as an unstaged concrete interpreter, a staged concrete interpreter, an unstaged abstract interpreter, or a staged abstract interpreter. As an example of abstraction without regret, the overhead of these abstraction layers is eliminated in the generated code after staging. We show that staging abstract interpreters is practical and useful to optimize static analysis, all while requiring less engineering effort and without compromising soundness. We conduct three case studies, including a comparison with Boucher and Feeley’s abstract compilation, applications to various control-flow analyses, and a demonstration for modular analysis. We also empirically evaluate the effect of staging on the execution time. The experiment shows an order of magnitude speedup with staging for control-flow analyses.

Wed 23 Oct
Times are displayed in time zone: (GMT+03:00) Beirut change

11:00 - 12:30: OOPSLA - Abstract Interpretation at Attica
Chair(s): John HughesChalmers University of Technology, Sweden
splash-2019-oopsla11:00 - 11:22
Zhuo ZhangPurdue University, Wei YouPurdue University, Guanhong TaoPurdue University, Guannan WeiPurdue University, Yonghwi KwonUniversity of Virginia, Xiangyu ZhangPurdue University
DOI Pre-print
splash-2019-oopsla11:22 - 11:45
Guannan WeiPurdue University, Yuxuan ChenPurdue University, Tiark RompfPurdue University
splash-2019-oopsla11:45 - 12:07
Benno SteinUniversity of Colorado Boulder, Benjamin Barslev NielsenAarhus University, Bor-Yuh Evan ChangUniversity of Colorado Boulder | Amazon, Anders MøllerAarhus University
DOI Pre-print
splash-2019-oopsla12:07 - 12:30
Sven KeidelJGU Mainz, Sebastian ErdwegJGU Mainz