We develop techniques and tools that exploit automated reasoning and large amounts of computing power to tackle challenging programming problems
We develop programming languages and systems to help programmers with a variety of tasks. We use program analysis and synthesis techniques to analyze a range of issues that include security vulnerabilities, creating controllers for dynamical systems, and enabling programmers to discover missing code.
A synthesis-enabled language that allows programmers to write programs with holes and then rely on constraint-based synthesis to discover the missing code.
Self-driving cars are likely to be safer, on average, than human-driven cars. But they may fail in new and catastrophic ways that a human driver could prevent. This project is designing a new architecture for a highly dependable self-driving car.
ACM SIGPLAN recently honored Armando Solar Lezama, MIT EECS professor and CSAIL Associate Director and Chief Operating Officer for his impactful work in program synthesis.
CSAIL researchers collaborated on the first neurosymbolic programming summer school at the California Institute of Technology, held from July 11 to 13.
