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).