Sparta: High-Performance Static Code Analyzers Based on Abstract Interpretation

What kinds of domains do you use when you run this on dex files?

IKOS has been originally designed to perform formal verification of embedded software and is heavily skewed toward numerical abstractions (intervals, octagons, interleaved widening/narrowing fixpoint iterator, etc.), which are computationally expensive. Since the goal is to verify critical pieces of software, it's OK to have an analysis take several hours to complete. Using IKOS also requires a deeper understanding of the theory Abstract Interpretation.

SPARTA has been designed with different goals in mind: speed and ease of use. The API is more streamlined and one can implement an analysis with minimal background in Abstract Interpretation. The algorithms in SPARTA have also been fine-tuned for maximum performance. SPARTA is meant to be used in compilers and optimizers, where speed of execution is critical.

Yes, writing transfer functions for dataflow analysis is your responsibility.

For anyone who comes across this in the future, this is a good way to understand the terms of abstract interpretation without getting a PhD.

https://wiki.mozilla.org/Abstract_Interpretation

It's a backend engine; it doesn't support languages out-of-the-box. That said, it's extensively used by the open-source Android bytecode optimizer [Redex](https://github.com/facebook/redex), so there's code readily available if you want to do Android bytecode analysis with SPARTA.