Overview

The Saturn project is exploring techniques for highly scalable and precise analysis of software, with applications to both bug-finding and verification. Saturn is based on three main ideas: In combination, these ideas give Saturn the ability to succinctly express precise analyses while also providing the ability to scale to very large programs. The use of constraints and logic programs allows succinct analyses, which are easier to understand and verify correct than analyses written at a lower level of abstraction. Bit-level path-sensitive analysis gives precision, while analyzing a single function at a time and summarization give scalability. As a result, we are able to routinely run whole-program Saturn analyses on the entire Linux kernel (with more than 6MLOC) and other large open source projects. Collectively these analyses have found thousands of previously unknown bugs in such projects, including projects that are already routinely checked by commercial bug-finding tools.

The current version of Saturn is a complete rewrite of the original system, which was developed starting in early 2004. As a result, the locking and memory leak bug-finding analyses, which were written in the old version, are not currently supported in the new version. The new version does provide a parallel implementation, allowing multiple functions to be analyzed at the same time; we generally use clusters of 25-80 processors, depending on program size and the computational intensity of the analysis. All Saturn analyses are currently for C programs, though the ideas could be applied to other languages.

Saturn is supported by NSF grants CCF-0430378 (which is partly funded by DARPA), CNS-050955, and SA4899-10808PG-1, and gifts or fellowships from IBM, Intel, and Microsoft.