This project provides open-source Medical Device Coordination
Framework (MDCF) for exploring solutions related to designing,
implementing, verifying, and certifying, systems of
integrated medical devices.
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.
Bogor is an Eclipse-ready extensible and customizable
framework for domain-specific model checking.
Cadena is a sophisticated Eclipse-based IDE for specification,
analysis, and development of distributed systems built using
the CORBA Component Model (CCM).
Indus is a collection of static analysis and program
transformation libraries for full Java that includes Kaveri
-- an Eclipse-based user interface that provides a number of
capabilities for computing program slices and navigating and
querying program dependence graphs.
JMLEclipse is, first and foremost, an Eclipse-based JML
front-end that provides JML infrastructure to process JML
specifications at source (JML2 syntax) and bytecode (embedded
JML Intermediate Representation -- JIR) levels.
Spec Patterns an online repository for information about
property specification for finite-state verification.
The intent of this repository is to collect patterns that
occur commonly in the specification of concurrent and
The project aims to use object-oriented methodologies to
design high-assurance systems using: (1) high-level, modular
specification of global, cross-cutting synchronization
aspects, (2) automatic derivation and weaving of verifiable
synchronization code, and (3) automated verification of
critical safety/liveness properties of woven code.