COMPUTER-AIDED PROGRAMMING

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

Cubix — Cubix is a framework for language-parametric source-to-source transformation. The ability to automatically rewrite code is critical for everything from automated refactoring to automated bug-fixing. Previous tools would need to be rewritten from scratch for each language because they lacked a way to handle the subtle variations between languages. We're making it possible to build tools that work on every language, and are just as good as tools written specifically for each language.
People: Jimmy Koppel

Mandate — If you write down the formal semantics of a programming language, it should be theoretically possible to automatically generate any tool you want for it. Mandate is a framework for doing this by performing rewrites and abstractions of rules. So far, we have focused on automatically synthesizing control-flow graph generators from operational semantics.
People: Jimmy Koppel

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