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
- Nathan Hunt, Scale AI
- Jack Feser, Hamilton College
- Jimmy Koppel
- Kliment Serafimov
- Ria Das, Basis
- 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