Scalable error detection using boolean satisfiability

Yichen Xie, Alex Aiken
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer] [url]
Read: 18 April 2021

Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
POPL '05
Long Beach, California, USA
Association for Computing Machinery
New York, NY, USA
Pages 351-363
2005
Note(s): lazy initialization, Saturn verifier, bounded model checking, CBMC verifier
Papers: ramos:sec:2015, engler:issta:2007, khurshid:tacas:2003, calcagno:popl:2009

Saturn is a SAT-based bug-finding tool for checking temporal logic formulae (expressed as state machines) on C programs and, in particular, for checking for locking errors in Linux kernel code. A key part of its design is the generation of function summaries using lazy initialization to infer the precondition of functions. It achieves a false positive rate of only 40%. A problem (that it shares with successors such as engler:issta:2007 and ramos:sec:2015) is its handling of pointer aliases: the function summaries generated are always trees, not DAGs.

Saturn is based on forward symbolic execution with merging at join points. Loops are handled by unrolling a bounded number of times. Function summaries are used to enable a bottom-up interprocedural analysis. That is, Saturn is a compositional bounded model checker.

Saturn uses BDDs to represent boolean formualae used as guards in order to simplify the guards generated at join points. Program slicing is used (but not thoroughly described).

When used on Linux, it generated 179 new bug reports involving locks.

The related work section is interesting. For example, comparing with CBMC, they emphasize the compositional analysis and the ability to use the particular errors being checked for to simplify the analysis and reduce the size of the function summaries: enabling Saturn to be used on very large codebases such as the Linux kernel. In contrast, they characterize CBMC as a whole-program assertion checker.

Lazy initialization of symbolic values

  • Compositional shape analysis by means of bi-abduction [calcagno:popl:2009]
  • Under-constrained execution: Making automatic code destruction easy and scalable [engler:issta:2007]
  • Generalized symbolic execution for model checking and testing [khurshid:tacas:2003]
  • Practical, low-effort equivalence verification of real code [ramos:cav:2011]
  • Under-constrained symbolic execution: Correctness checking for real code [ramos:sec:2015]