Easy Abstract Interpretation with SPARTA
Arnaud Venet, Jez Ng at Strange Loop 2019
Using abstract interpretation to build a scalable tool from scratch is a daunting engineering task that generally requires a protracted development effort. To streamline that process, we built (SPARTA)1, a C++ library of components for building high-performance static analyzers that can run in a production environment. SPARTA provides the building blocks so an engineer can focus solely on the logic that extracts the desired information from the program. The library ensures that the resulting analysis is sound, efficient, and scalable.
SPARTA is actively used by Facebook, most notably in our open-source Android bytecode optimizing compiler Redex. However, SPARTA is language-independent and contains no Android-specific logic.
In this talk we will go over some of the algorithms behind SPARTA, the benefits we've obtained, and we will show you how to use it in your own analyses.
Arnaud Venet
Facebook
Arnaud got his PhD in abstract interpretation from the École Polytechnique in 1998 and has helped spread the use of scalable static analysis in industry since then.
Jez Ng
Facebook
Jez has been hacking on programming languages and runtimes at Facebook for the past five years: first on the Hack typechecker and then on the Redex optimizing compiler for Android. While an undergraduate at Amherst College, he also worked on Doppio, one of the first JVM implementations in the browser.
SPARTA is actively used by Facebook, most notably in our open-source Android bytecode optimizing compiler Redex. However, SPARTA is language-independent and contains no Android-specific logic.
In this talk we will go over some of the algorithms behind SPARTA, the benefits we've obtained, and we will show you how to use it in your own analyses.
Arnaud Venet
Arnaud got his PhD in abstract interpretation from the École Polytechnique in 1998 and has helped spread the use of scalable static analysis in industry since then.
Jez Ng
Jez has been hacking on programming languages and runtimes at Facebook for the past five years: first on the Hack typechecker and then on the Redex optimizing compiler for Android. While an undergraduate at Amherst College, he also worked on Doppio, one of the first JVM implementations in the browser.