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