Current Projects

MDCF Integrated Medical Devices

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.

Sireum A Software Analysis Platform

Sireum is a long-term research effort to develop an over-arching software analysis platform that incorporates various static analysis techniques such as data-flow framework, model checking, symbolic execution, abstract interpretation, and deductive reasoning techniques.


Past Projects

Bandera Java Software Model Checking

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 A Software Model Checking Framework

Bogor is an Eclipse-ready extensible and customizable model checking engine for object-oriented (OO) software.

Cadena IDE for Component-based Systems

Cadena is a sophisticated Eclipse-based IDE for specification, analysis, and development of distributed systems built using the CORBA Component Model (CCM).

Indus Static Analyzers and Slicer for Concurrent Java

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 Java Modeling Language (JML) Tools

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
Spec Patterns Property Specification Patterns

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 reactive systems.

SyncGen Synchronization Synthesizer

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.