Summary: Saturn: A Scalable Framework for Error Detection
using Boolean Satisfiability
Yichen Xie and Alex Aiken
This article presents Saturn, a general framework for building precise and scalable static error
detection systems. Saturn exploits recent advances in boolean satisfiability (SAT) solvers and is
path sensitive, precise down to the bit level, and models pointers and heap data. Our approach
is also highly scalable, which we achieve using two techniques. First, for each program function,
several optimizations compress the size of the boolean formulas that model the control- and data-
flow and the heap locations accessed by a function. Second, summaries in the spirit of type
signatures are computed for each function, allowing inter-procedural analysis without a dramatic
increase in the size of the boolean constraints to be solved.
We have experimentally validated our approach by conducting two case studies involving a
Linux lock checker and a memory leak checker. Results from the experiments show that our
system scales well, parallelizes well, and finds more errors with fewer false positives than previous
static error detection systems.
Categories and Subject Descriptors: D.2.4 [Software Engineering]: Software/Program Verifi-
cation; D.2.3 [Software Engineering]: Coding Tools and Techniques; D.2.5 [Software Engi-
neering]: Testing and Debugging
General Terms: Algorithms, Experimentation, Languages, Verification.