COMPUTER-AIDED PROGRAMMING

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

PROJECTS

Sketch — A synthesis-enabled language that allows programmers to write programs with holes and then use constraint-based synthesis to discover the missing code.
People: Armando Solar-Lezama

Castor — A deductive synthesis tool that generates workload-specialized database implementations. Starting from a set of SQL queries, Castor generates a specialized data layout that supports efficient execution of the queries.
People: Jack Feser

SyMetric — SyMetric is a synthesis tool that uses distance functions between programs to prune the program search space, enabling efficient synthesis in difficult domains such as inverse constructive solid geometry.
People: Jack Feser

VSRL — VSRL stands for verifiably safe reinforcement learning. Given sufficient information about the unsafe objects and dynamics in an environment, VSRL enables you to train a reinforcement learning agent while provably preserving safety properties throughout training.
People: Nathan Hunt

PUBLICATIONS

ALUMNI