About
The SAFE (Scalable And Flexible Error detection and verification) project develops software for verification of Java programs. SAFE verifies that a Java program satisfies a particular set of specifications. SAFE applies static program analysis, a set of methods to analyze
source code or object code, without requiring execution of the program.
You can also visit the original SAFE page at IBM, which I no longer maintain.
Typestate checking in the presence of aliasing
Our research has focused heavily on precise typestate checking in the presence of aliasing. In the typestate model, objects of a given type exist in one of finitely many states. The operations (i.e., method calls) permitted on an object depend on its state, and the operations can potentially alter an object's state. Typestate verification attempts to statically determine if the execution of a given program may cause an operation to be performed on an object in a state where the operation is not permitted.
Typestate checking can be used to verify that objects satisfy certain kinds of temporal properties; e.g., that an object is not used before it is initialized, or that a resource is not used after it is closed.
One of the principal difficulties in performing precise typestate checking (and software verification in general) arises from determining how aliasing interacts with operations on objects.
The goal of SAFE is to provide a scalable and flexible error-detection tool, based on typestate checking with varying degrees of cost and precision, mostly depending on the way in which aliasing is handled.
SAFE can be used for detecting violations of simple correctness properties, and for checking more sophisticated performance properties such as inefficient use of resources.
