Saturn Main Page

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 ultimately used these techniques to (come close to) verifying properties of a full operating system (see the Oakland 2008 paper).

News

With the release of Version 1.2 we are happy to declare the successful conclusion of the Saturn project; thanks everyone!
Important caveat: The manual and tutorial have not been updated to reflect the changes in version 1.2. If you are just learning Saturn and want to work through the tutorial you should start with an earlier verson. Much of what has changed in the interfaces in Version 1.2 is discussed in chapters 3 and 5 of this thesis.
Saturn 1.2 is now available.
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).