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 work