Our goal is to find better ways to make software, and ways to make software better.
We're inventing new programming paradigms (Déjà Vu, Espalier) so that end users can create more sophisticated apps themselves, and programmers can build more flexible complex systems with less code. We're developing a new theory of software design, which focuses not on the question of how to implement, but on the harder question of what to implement (and how to tell in advance if it's likely to be usable).
We've been working for a while on software security for web and mobile applications; we're now beginning a new project on cyberphysical systems. We continue to support and extend the Alloy modeling language and analyzer, still the only tool to provide fully automatic analysis of software designs that involve rich state.
Our research style is principled, practical and irreverent: we don't pay much attention to all the assumptions that are usually made in software engineering and programming languages (e.g., that only code matters, that proving things correct means that they work right, or that the most important engineering questions can be answered empirically).
If you're interested in a UROP or MEng position, please see the list of available projects and contact the leader of the specific project you'd like to join.
Wildcard is a platform that empowers anyone to build browser extensions and modify websites to meet their own specific needs, using a familiar spreadsheet view.
Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. Hundreds of projects have used Alloy for design analysis, for verification, for simulation, and as a backend for many other kinds of analysis and synthesis tools, and Alloy is currently being taught in courses worldwide.
Self-driving cars are likely to be safer, on average, than human-driven cars. But they may fail in new and catastrophic ways that a human driver could prevent. This project is designing a new architecture for a highly dependable self-driving car.
Even formally verified protocols that have been faithfully implemented have been found to have security vulnerabilities. A new framework eliminates such vulnerabilities by design.
What is design thinking in the context of software? We're developing a new approach to software design that achieves usability and robustness by going deeper than the user interface.
Déjà Vu is a new platform for end-user development of apps with rich functionality. It features a novel theory of modularity for binding concepts; an extensive library of reusable concepts; and a WYSIWYG tool for specifying bindings and customizing visual layout
An approach to reducing risks of attack on cyberphysical infrastructure (such as water purification plants and electric grids) with new software design and analysis techniques.
Espalier (formerly Object Spreadsheets) is a new computational paradigm that combines the usability advantages of spreadsheets with SQL-like expressive power, providing a way to build a wide class of interactive applications more easily than with existing tools.
