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.

Thanks to the generosity of IBM, SAFE is open-source under the Eclipse Public License.

Get the source code!

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.

Publications

Static Specification Mining using Automata-Based Abstractions
Yahav E., Shoham S., Fink S., Pistoia M.
Book chapter: Mining Software Specifications: Methodologies and Applications
The SAFE Experience
Yahav E., Fink S.
In Engineering of Software 2011, Part 1
[pdf]
Static Specification Mining Using Automata-Based Abstractions
Shoham S., Yahav E., Fink S., Pistoia M.
IEEE Transactions on Software Engineering (TSE 2008).
Generating Precise and Concise Procedure Summaries
Yorsh G., Yahav E., Chandra S.
POPL'08: ACM Symposium on Principles of Programming Languages
[bib] [abstract] [ps] [pdf] [slides]
Verifying Dereference Safety via Expanding-Scope Analysis
Loginov A., Yahav E., Chandra S., Fink S., Rinetzky N., Nanda M. G.
ISSTA '08: International Symposium on Software Testing and Analysis
[bib] [abstract] [pdf] [slides]
The CLOSER: Automating Resource Management in Java
Dillig I., Dillig T., Yahav E., Chandra S.
ISMM '08: 2008 International Symposium on Memory Management
[bib] [abstract] [pdf] [slides]
Effective Typestate Verification in the Presence of Aliasing
Fink S.J., Yahav E., Dor N., Ramalingam G., and Geay E.
ACM Transactions on Software Engineering and Methodology 2008 (TOSEM).
When Role Models Have Flaws: Static Validation of Enterprise Security Policies
Pistoia M., Fink S.J., Flynn R.J., and Yahav E.
ICSE '07: 29th Int. Conference on Software Engineering.
[bib] [pdf] [slides]
Static Specification Mining Using Automata-Based Abstractions
Shoham S., Yahav E., Fink S., Pistoia M.
ISSTA'07: International Symposium on Software Testing and Analysis 2007
Best paper award
[bib] [abstract] [ps] [pdf] [slides]
Effective Typestate Verification in the Presence of Aliasing
Fink S.J., Yahav E., Dor N., Ramalingam G., and Geay E.
ISSTA '06: International Symposium on Software Testing and Analysis
Best paper award
[bib] [abstract] [ps] [pdf] [slides]
Continuous code-quality assurance with SAFE
Geay E., Yahav E., Fink S.J.
PEPM 2006: ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program Manipulation
[bib][abstract] [pdf]
Typestate Verification: Abstraction Techniques and Complexity Results
Field J., Goyal D., Ramalingam G., and Yahav E., 
Science of Computer Programming, Volume 58, Issues 1--2, pages 57--82, October 2005
Typestate Verification: Abstraction Techniques and Complexity Results,
Field J., Goyal D., Ramalingam G., and Yahav E., 
SAS '03  [bib] [abstract] [ps] [pdf] [slides]