About SpEx-JML

SpEx-JML is an effort to verify JML specifications from Java programs, by using Bogor as the underlying checking engine. This is not the first time a similar effort has been done, as shown by the works at LOOP, ESC/Java, ChAsE, JACK, etc. The main difference between SpEx-JML and these efforts is that, unlike most of this tool which use static analysis, SpEx-JML checkings are done dynamically, which gives it an extra amount of power at the time of performing the analysis.

Being able to perform dynamic analysis has a number of advantages (and also disadvantages). For example, the fact that SpEx-JML can use Bogor's internal and dynamic representation of the heap at every program point to perform analysis, implies that its checking for assignable clauses is both sound and complete (with respect to the current environment). However, as it is well known, model-checking can be very expensive due to the state-space-explosion phenomenon. This, plus the overhead of checking JML constructs can be a potential problem for this technique. This is where Bogor, an extremely flexible model-checking framework with state-of-the-art reduction algorithms, comes into play by reducing the overhead of checking JML to tolerable levels (even vanishing it all, space-wise speaking, in some cases).

For more information, refer to SpEx-JML paper "Checking Strong Specifications Using An Extensible Software Model Checking Framework" in the papers section.