Bounded Program Verification
Bounded Program Verification
ABOUT FORGEForge is a program analysis framework that allows a procedure in a conventional object oriented language to be automatically checked against a rich interface specification. The framework uses a bounded verification technique, in which all executions of a procedure are examined up to a user-provided bound on the heap and number of loop unrollings. If a counterexamples exists within the bound, Forge will find and report the complete program trace, but defects outside the bound may be missed. To facilitate modular analysis, specifications can be embedded as statements in code, an idea borrowed from the refinement calculus. The core Forge library, available for download on this page, operates on programs constructed in the Forge Intermediate Representation (FIR), a simple, relational programming language. To analyze a program written in a conventional programming language, like Java or C, that program and its specification must first be encoded in FIR. We have built a command-line tool called JForge that analyzes Java code against specifications written in the Java Modeling Language (JML) by translating them both to FIR, and we have made this tool available for download as well. Others are working on a translation from C to FIR, and we welcome and encourage you to encode your own favorite language in FIR. When other unsound static analyses, such as ESC/Java2, fail to find counterexamples, they do not report which program behaviors the analysis may have failed to cover. This stands in contrast to testing, in which coverage metrics can measure how thoroughly the program was exercised and which, in turn, help the user craft a more comprehensive test suite. We are working to extend Forge with such a coverage metric, and it is the design and evaluation of the metric that is the major challenge remaining in this project. PUBLICATIONSGreg Dennis, Felix Chang, Daniel Jackson. Modular Verification of Code with SAT. International Symposium on Software Testing and Analysis. Portland, ME, July 2006. (PDF) (PS) Greg Dennis, Kuat Yessenov, Daniel Jackson. A Relational Framework for Bounded Program Verification of Object-Oriented Programs. Submitted for Publication, December 2007. |
DOWNLOADForge and JForge are licensed under the GNU General Public License, Version 3. If this license doesn't suit your needs, contact us to discuss. Download the Forge binary: forge.jar (last updated: 03/13/08) Download the JForge release: jforge.tar.gz (last updated: 03/13/08) The default SAT Solver used by Forge and JForge is SAT4J, which is pure Java. We highly recommend you use one of the other supported SAT solvers, because they usually exhibit better performance. To use a SAT solver besides SAT4J, you must visit the Kodkod website to download the platform-specific binaries and follow the example for adding those binaries to the Java library path. DOCUMENTATIONRead the FIR Primer. Read the JForge tutorial. View the Forge API Documentation. ACKNOWLEDGEMENTSThis research was supported by the National Science Foundation under Grant No. 0541183 (Deep and Scalable Analysis of Software). Forge uses the Kodkod model finder and SAT4J 1.7. MEMBERSGreg Dennis (main contact) |
