About SpEx

SpEx (Specifications Exploration) is a project which main objective is the study of different specification formalisms in terms of several factors like: expressiveness, automation potential, domain adequacy, etc., and also their suitability for different verification techniques, for example, model checking, static analysis, and so on. These studies drive the development of verification techniques for the languages studied or even the proposal for extensions of such languages with new constructs that address possible weaknesses.

The first phase of SpEx has been targeted to checking JML specifications by means of model checking. Using Bogor's flexible framework, we were able to write extensions to check complex runtime properties of the heap and some properties involving quantification over elements of data structures. This, together with the ability to check pre and post conditions, allowed us to be able to check a rich subset of JML specifications that had not been possible to check by other tools in the past. The work on JML specifications is still in progress and we are currently working on acheiving total covering of the language and studying its appropriateness in a multi-threaded concurrent setting. For more information on JML specification extensions, please visit the documentation section.

Although JML currently constitutes the major research effort in SpEx, future work includes checking OCL specifications and enabling the check of temporal properties (although SpEx current support of JML's \old construct already allows the check of some simple temporal behavior).

If you are interested in reading this information in the Belorussian language, you can find a nice translation here