Facebook has opened its incubator once again, offering developers SPARTA – a library for building static analysers based on abstract interpretation.

Static analysers is used to find bugs in programs without actually running them, but just examining the code. Tools using abstract interpretation produce output that has all possible execution contexts considered. Since the failed launch of Ariane 501, they are, for example, often used for programme analysis in the aerospace industry.

While some might associate the name with an ancient greek city whose inhabitants sport a taste for fighting, SPARTA stands for Semantics, PARTitioning and Abstraction, which Facebook described as “the three fundamental axes in the design of an analysis”. It is a header-only C++ library, which provides data structures such as finite lattices and abstract environments to use as the foundation for scalable static analysis tools.

The main aim of the project is to ensure that the analysers built with it are fast and mathematically sound. As the introductory blog post suggests, SPARTA is part of an initiative to use more abstract interpretation in the company’s tools. It can for example be found in Facebook’s ReDex code optimiser for Android.

By sharing the source code, which is MIT licensed and can be found on GitHub, Facebook invites company outsiders to contribute additional algorithms and abstractions.

Future plans include support for numerical abstractions and points-to analysis, but since the announcement is very carefully worded in this regard, you probably shouldn’t bet on those appearing any time soon.

SPARTA requires v1.58 or a later version of the Boost library to work. To help anyone interested in the project make the most of it, its developers have included code samples and typical use cases within the library. A look at the unit test included can also help to get started implementing an analysis.