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.
sub: amandroid

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 framework for domain-specific model checking.

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: 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.