Thu 29 Oct 2015 16:42 - 17:06 at Grand Station 1 - 8. Static Analysis Chair(s): Werner Dietl

The design and implementation of static analyzers has become increasingly systematic. Yet for a given language or analysis feature, it often requires tedious and error prone work to implement an analyzer and prove it sound. In short, static analysis features and their proofs of soundness do not compose well, causing a dearth of reuse in both implementation and metatheory. We solve the problem of systematically constructing static analyzers by introducing Galois transformers: monad transformers that transport Galois connection properties. In concert with a monadic interpreter, we define a library of monad transformers that implement building blocks for classic analysis parameters like context, path, and heap (in)sensitivity. Moreover, these can be composed together independent of the language being analyzed. Significantly, a Galois transformer can be proved sound once and for all, making it a reusable analysis component. As new analysis features and abstractions are developed and mixed in, soundness proofs need not be reconstructed, as the composition of a monad transformer stack is sound by virtue of its constituents. Galois transformers provide a viable foundation for reusable and composable metatheory for program analysis. Finally, these Galois transformers shift the level of abstraction in analysis design and implementation to a level where non-specialists have the ability to synthesize sound analyzers over a number of parameters.

Thu 29 Oct

oopsla2015
15:30 - 17:30: OOPSLA - 8. Static Analysis at Grand Station 1
Chair(s): Werner DietlUniversity of Waterloo
oopsla201515:30 - 15:54
Talk
Magnus MadsenUniversity of Waterloo, Frank TipSamsung Research America, Ondřej LhotákUniversity of Waterloo
DOI Media Attached
oopsla201515:54 - 16:18
Talk
Yu FengUniversity of Texas at Austin, USA, Xinyu WangUT Austin, Isil DilligUniversity of Texas at Austin, USA, Calvin LinUniversity of Texas at Austin, USA
Pre-print Media Attached
oopsla201516:18 - 16:42
Talk
Jens DietrichMassey University, New Zealand, Nicholas HollingumUniversity of Sydney, Australia, Bernhard ScholzOracle Labs, Australia
DOI Media Attached
oopsla201516:42 - 17:06
Talk
David DaraisUniversity of Maryland, College Park, Matthew MightUniversity of Utah, USA, David Van HornUniversity of Maryland at College Park, USA
DOI Media Attached
oopsla201517:06 - 17:30
Talk
Hakjoo OhKorea University, South Korea, Hongseok YangUniversity of Oxford, UK, Kwangkeun YiSeoul National University, South Korea
DOI Media Attached