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
PUBLICATIONS
ALUMNI
- Kliment Serafimov
- Ria Das
- Jeevana Inala, Microsoft Research
- Zenna Tavares, Columbia University
- Evan Pu, Autodesk Research
- Kevin Ellis, Cornell
- Xin Zhang, Peking University
- Osbert Bastani, UPenn
- Nadia Polikarpova, UCSD
- Sicun Gao, UCSD
- Shachar Itzhaky, Technion
- Rohit Singh, Citadel
- Xiaokang Qiu, Purdue University
- Zhilei Xu, Google
- Kuat Yessenov, Google
- Jean Yang, Akita Software
- Rishabh Singh, Google Brain
- Alvin Cheung, University of Washington