We develop techniques and tools that exploit automated reasoning and large amounts of computing power to tackle challenging programming problems

We develop programming languages and systems to help programmers with a variety of tasks. We use program analysis and synthesis techniques to analyze a range of issues that include security vulnerabilities, creating controllers for dynamical systems, and enabling programmers to discover missing code. 

A synthesis-enabled language that allows programmers to write programs with holes and then rely on constraint-based synthesis to discover the missing code.

We've developed languages such as Sketch, Jeeves and Sigma.

Impact Areas