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 Filesystem 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 |
|---|---|
| Proton Therapy Control Center | 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 |