The goal of the Saturn project is to statically and automatically
verify properties of large (meaning multi-million line) software
systems. The focus of much of our work is simultaneously achieving
scalability, precision, and a straightforward way of
expressing analyses that is easy to reason about; see the
overview for more details.
We plan to use these techniques to verify properties of a full
operating system.
News
- Saturn 1.1 is now available.
- Saturn 1.0 is available. In addition to the base Saturn infrastructure,
this release includes a sound alias analysis,
an unsound (bug-finding) null dereference analysis for C programs.
Both analyses are context-, flow-, and
partially path-sensitive and scale to the entire Linux kernel (i.e.,
configured with all device drivers).