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. 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. 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. Bounded Verification of Voting Software. Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2008) . Toronto, Canada, October 2008. (PDF) MEMBERS |
TOOLSForge, JForge, and JMLForge are licensed under the GNU General Public License, Version 3. If this license doesn't suit your needs, contact us to discuss. Install the JForge Eclipse plugin with this update site URL. (version: 0.2.6; last updated: 12/1/09) Download the Forge binary: forge.jar. (last updated: 7/29/09) Download the JMLForge release: jmlforge.tar.gz. (last updated: 09/09/08) The default SAT Solver used by our tools 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 about the JForge Eclipse plugin. Read the FIR Primer. Read the JMLForge 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) and the Toshiba Corporate Research and Development Center. Forge uses the Kodkod model finder and SAT4J. |
