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