Principal Investigator Daniel Jackson
Co-investigators Jonathan Edwards , Sol J Greenspan
Project Website http://sdg.csail.mit.edu/forge/
Checking programs against rich interface specifications, memory usage constraints, and temporal logic properties.
Forge Bounded Program Verification -- 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.
When other unsound static analyses fail to find counterexamples, they usually 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 have extended Forge with such a coverage metric that reports the degree to which each the code and the specification were covered by the analysis.
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 JForge, a Java front-end to Forge, which is an Eclipse plugin that analyzes Java against specifications written in a relational first-order logic similar to Alloy, by translating both to FIR.
We also offer JMLForge, a command-line tool that checks Java against specifications written in the Java Modeling Language (JML), but it is not as advanced as JForge and not being actively supported. Engineers at the Toshiba Corporate Research and Development Center are currently developing a translation from C to FIR, and we welcome and encourage you to encode your own favorite language in FIR as well.