Computer Science and Artificial Intelligence Laboratory

The research of the Software Design Group is currently supported by grants from the National Science Foundation, from the Air Force Research Laboratory and Disruptive Technology Office, from the Nokia Corporation, and from the Toshiba Corporation.



Alloy Technology

Designing the Alloy logic, language, and analysis and related tools and case studies.

Ongoing Projects Past Projects
Alloy Analyzer Modeling By Example
Kodkod Model Finder Declarative Course Scheduler
Generating Code from Alloy
Flash File System Design and Analysis

Program Analysis and Verification

Checking programs against rich interface specifications, memory usage constraints, and temporal logic properties.

Ongoing Projects Past Projects
Forge Bounded Verification Automatic Test-Case Generation
Karun Specification Inference Jalloy Bug Finder
Memory Leak Detection Model-Checking Declarative Relational Models
Model-Checking Heuristics

Safety-Critical Systems

Constructing safety arguments for critical systems, including proton therapy machines and air traffic control tools.

Ongoing Projects Past Projects
Software Dependability for Proton Therapy Direct-To
TSAFE
FIG

Programming Language Design

Designing novel programming languages founded upon relational semantics.

Ongoing Projects Past Projects
Subtext Aaree
Imperative/Declarative Hybrid Languages

Design Extraction

Extracting design properties of code to aid program understanding.

Ongoing Projects Past Projects
Object Ownership Inference Womble Object Model Extraction