Bandera
[more...]
The Bandera project addresses one of the major obstacles in the path of practical finite-state verification of software. Tools like SMV and SPIN accept a description of a finite-state transition system as input. Bridging the semantic gap between a non-finite-state software system expressed as source code and those tool input languages requires the application of sophisticated program analysis, abstraction, and transformation techniques.
The goal of the Bandera project is to integrate existing programming language processing techniques with newly developed techniques to provide automated support for the extraction of safe, compact, finite-state models that are suitable for verification from Java source code. While our ultimate goal is fully-automated model extraction for a broad class of software systems, our approach takes as a given that guidance from a software analyst may be required.
Cadena
[more...]
The Cadena project is the use of component models such as Enterprise Java Beans and the CORBA Component Model (CCM) in application development is expanding rapidly. Even in real-time safety/mission-critical domains, component-based development is beginning to take hold as a mechanism for incorporating non-functional aspects such as real-time, quality-of-service, and distribution.
Bogor
[more...]
Bogor is an extensible software model checking framework with state of the art software model checking algorithms, visualizations, and user interface designed to support both general purpose and domain-specific software model checking. Although there are many model checkers available, Bogor provides a number novel capabilities that make it especially well-suited for checking properties of a variety modern software artifacts, for building your own domain-specific engine, and for using it to teach model checking concepts.
Indus [more...]
Indus is an effort to provide a collection of program analyses and transformations implemented in Java to customize and adapt Java programs.
JMLEclipse [more...]
The whole idea behind JMLEclipse is to have an open framework that can be used as frontend for different JML tools. These frontend provides well-formedness checking and syntax highlighting aid, and other tools can connect as backends, using an open interface, to provide further analysis of JML annotated programs.
SpEx [more...]
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.
Sensor Network [more...]
This project aims to develop a framework for model-driven, product line-based design and implementation of sensor network applications. The framework will include model-driven analysis tools to aid the designer in configuration and selection of protocols and protocol parameters, and simulation engine plug-ins to evaluate design choices.