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