Title: Scaling the Symbolic Reasoning Stack
Advisors: Emina Torlak, Dan Grossman, and Luis Ceze
Supervisory Committee: Emina Torlak (co-Chair), Dan Grossman (co-Chair), Luis Ceze (co-Chair), Amy Ko (GSR, iSchool), Xi Wang, and Ras Bodik
Abstract: Symbolic reasoning tools, including those based on program synthesis, have successfully solved challenging tasks in a variety of application domains, from compilers to consistency models. But developing a symbolic reasoning tool that scales to large problems requires considerable expertise—implementing search procedures from scratch and a thorough understanding of the underlying engine—that limits the reach of synthesis technology. My thesis is that new abstractions and interfaces can help programmers to build scalable symbolic reasoning tools. I propose three contributions to scale the symbolic reasoning stack: metasketches to specify search strategies to a reusable synthesis engine, symbolic profiling to understand and optimize the behavior of a symbolic tool, and profile-guided symbolic execution to automatically optimize compilation to constraints. I have demonstrated the effectiveness of these contributions in several domains, including a new tool for synthesizing memory consistency models.