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 |