Software Design Group

The Alloy Analyzer is a tool for modeling and analyzing software systems. It has been used in a variety of applications, including bug finding, network protocols, security analysis, configuration, and requirements analysis.

Event-based Synthesis

The goal of this project is to synthesize distributed applications from declarative event-based specifications.

Knowledge-Driven Security Analysis

The goal of this project is to construct a database of existing security knowledge (exploits, vulnerabilities, mitigations, etc.) and automatically leverage them for security analysis. Case studies include the Apache Server security, router configuration, social networks, and web security protocols.

Kodkod is a model finder for first-order relational logic. It is capable of finding a satisfying instance to a set of constraints, and if no such instance exists, extracting a minimal unsatisfiable core. Among its numerous applications, it serves as the underlying analysis engine for the Alloy Analyzer.

Rubicon is a tool for analyzing Ruby on Rails programs. It allows programmers to extend existing RSpec tests with logical quantifiers, enabling exhaustive analysis of a Rails application.

Squander is a system for executing declarative specifications inside programs. Given a declarative specification of a method, Squander allows programmers to execute the method without providing an implementation.

Subtext is a new programming language designed to liberate programmers from the complexity and nuisance of programming with mutable states.