Forge Analysis Architecture
The trace produced by Forge is guaranteed to be an actual trace of the code that violates the provided specification. However, counterexamples may be missed if they fall outside the bounds provided by the user. Thus, we call this analysis a bounded verification.
Our technique is intended to be used as a modular, not a whole program, analysis. Because the analysis checks a procedure in isolation against its specification, accounting for all possible contexts of use, that specification can then be assumed in place of the procedure when analyzing client code. As a result, large coded bases can be checked in a modular, incremental fashion.
We have used Forge to check a variety of linked list implementations
java.util.List interface against the JML specification
List . The implementations were drawn from the Sun
Collections Framework, the GNU Trove library, the Apache Jakarta Commons-Collections
library, and some variants of the Sun implementation that had been seeded
with bugs for an MIT software engineering class. The tool revealed all
the seeded bugs and a previously unknown bug in the GNU Trove library.
Our current challenge is applying the tool to verify vote-tallying code used by the nation of the Netherlands. We also hope to incorporate Taghdiri's specification inference techniques   into Forge to reduce the need for writing specifications of called procedures.
This work is supported in part by the National Science Foundation (Deep and Scalable Analysis of Software, Award 0541183).
 G. Dennis, F. S. Chang, and D. Jackson. Modular Verification of Code with SAT. International Symposium on Software Testing and Analysis (ISSTA '06), Portland, Maine, July 2006.
 E. Torlak and D. Jackson. Kodkod: A Relational Model Finder. Tools and Algorithms for Construction and Analysis of Systems (TACAS '07), Braga, Portugal, March 2007.
 D. Jackson. Object Models as Heap Invariants. Essays on Programming Methodology, edited by Carroll Morgan and Annabelle McIver, Springer Verlag, 2000.
 The Java Modeling Language. http://www.cs.iastate.edu/~leavens/JML/
 M. Taghdiri. Inferring Specifications to Detect Errors in Code. International Conference on Automated Software Engineering (ASE '04), Linz, Austria, September 2004.
 M. Taghdiri, R. Seater, and D. Jackson. Lightweight Extraction of Syntactic Specifications. International Symposium on Foundations of Software Engineering (FSE'06), Portland, Oregon, November, 2006.
Computer Science and Artificial Intelligence Laboratory (CSAIL)
The Stata Center, Building 32 - 32 Vassar Street - Cambridge, MA 02139 - USA
tel:+1-617-253-0073 - firstname.lastname@example.org