The field of program analysis is experiencing a renaissance as recent software
analyzers have succeeded in verifying the correctness, safety and integrity of
increasingly large software systems. Progress in the design of real-world
analyzers comes from exploring the vast design space, however the process for
designing and implementing static analyzers with non-standard features has
grown too complex. Worse, changing the design of a static analyzer in
mid-development often requires a redesign from scratch.

In this talk I will present Galois transformers, a framework which supports
rapid design and implementation of a large family of static analyzers. Galois
transformers synthesize analysis machinery and proofs of correctness for free,
and are inspired by the trifecta combination of monad transformers, Galois
connections and monadic abstract interpreters. Galois transformers enable the
designer of a program analysis to rapidly prototype variations in abstract
domain, context sensitivity, object sensitivity, path sensitivity and a wide
range of analysis optimizations. Furthermore, these orthogonal tuning knobs are
constructed in a language-independent framework, allowing reuse across entirely
different programming language semantics. Finally, Galois transformers
synthesize a large portion of the end-to-end proofs of correct abstraction
required by high-assurance analyzers.