SAFE

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. SAFE provides a wide variety of program checkers. In particular, it provides a "structural checker" verifying simple structural properties, and a "typestate checker" verifying deeper properties using a more precise analysis.

SAFE can be easily used in continuous integration tools. It has been integrated into CruiseControl, and also provides a command line mode, an Ant task, and Eclipse integration.

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.

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]

From the integration within Eclipse, you can take a look at how the different analyzers can be executed. Run typestate checker Run structural checker Results are collected within Analysis Results view.