Saturn is available for download. The final release, Version 1.2, contains a suite of new analyses for checking type safety and analyzing the heap in large systems. Note that the interfaces in Version 1.2 have changed from 1.1; thus, 1.1 analyses may need some updating to run under 1.2. The most significant difference is in the treatment of aliasing in the memory model. Previously (in 1.1), abstract memory locations were given a single unique name among all the different potential aliases to the location. In 1.2 there is no distinguished name for a memory location and one asks explicit queries to learn whether two names (access paths) may be aliased. This change makes Saturn more consistent with standard approaches for describing alias analysis.
The easiest way to get and install Saturn is to use Philip Guo's fully encapsulated version, built using his tool
CDEpack. As long as you have a pretty standard Linux configuration, this version will install and just work. You can get Saturn 1.2
If for some reason you really want to install Saturn yourself or use an older version, the links below take you to
all the historical releases.
We strongly encourage anyone using Saturn to subscribe to the mailing lists for announcements about and discussion of Saturn.
- The Saturn infrastructure, including everything necessary to write analyses for C programs.
- A manual with a tutorial and reference documentation. Note: The manual/tutorial have not been updated for version 1.2; if you want to work through the tutorial use version 1.1
- A sound context-, flow-, and partially path-sensitive alias analysis for C, that scales to the entire Linux kernel. A paper on the alias analysis is available.
- An unsound, bug-finding (but nevertheless effective) null dereference analysis for C programs that also scales to Linux (not included in 1.2).