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).