Welcome to the Software Design Group
The Software Design Group does research in many areas of software engineering, including: design languages and analysis, extraction of designs from code, checking conformance of code to designs, and automatic test case generation.
Our philosophy is to couple lightweight design and specification notations with powerful tools. Much of our work in the last few years has revolved around Alloy, a declarative language for modelling software systems that manipulate complex structures, and the Alloy Analyzer, a SAT-based simulator and checker for Alloy. Alloy has been used to find flaws in published designs of several systems, and has been taught in over a dozen universities. One recent application of Kodkod, the newest Alloy relational engine, is a course scheduler for figuring out what courses to take each semester in order to complete a given MIT degree on time.
We develop and evaluate our ideas in the context of real software systems, including the control software of the proton therapy machine at Massachusetts General Hospital and the software used in Nokia cell phones. In previous work, we analyzed an air-traffic control system built by NASA and deployed in several US airports.
You can learn more about our group by following the links on the left.