APT

Automated program transformations for synthesis and analysis.

DerivationMiner

Mining formal stepwise refinement derivations.

Specware

Transformation-based general-purpose synthesis.

HACMS

High-assurance TCP/IP protocol stack.

CRASH

Synthesis of concurrent garbage collectors.

Diversity

Using software generation and repair for cyber-defense.

APAC

Sound static analysis of Android apps, to exclude malware.

VIBRANCE

Automatic removal of security vulnerabilities from Java applications.

vTPM

Formal modeling, proofs, and synthesis of a virtual Trusted Platform Module.

Hyperproperties

Investigating approaches to refinement that handle hyperproperties.

Constraintware

Synthesis of high-performance constraint solvers.

F6

Design and formal verification of a multi-level secure, fault-tolerant software platform for fractionated satellites.

JCRE

Synthesis of an embedded smart card operating system.

AutoSmart

Automatic generation of high-assurance smart card applications.

Java

Synthesis of a Java bytecode verifier.

PDA

A security protocol derivation assistant.

Planware

Domain-specific planning and scheduling.

EDCS

Evolution based on precise semantic design records.

KIDS

Automated support for the development of correct and efficient programs from formal specifications

DTRE

Data Type Refinement Environment.