The SAFE Experience
The authors present an overview of the techniques developed under the SAFE project. The goal of SAFE was to create a practical lightweight framework to verify simple properties of realistic Java applications. The work on SAFE covered a lot of ground, starting from typestate verification techniques, through inference of typestate specifications, checking for absence of null derefences, automatic resource disposal, and an attempt at modular typestate analysis. In many ways, SAFE represents a modern incarnation of early ideas on the use of static analysis for software reliability.