CAREER: The Next 700 Solver-Aided Languages

University Of Washington, Seattle WA

Investigators

Abstract

Software is a critical part of modern infrastructure, and programming is an essential part of knowledge work in many fields, from physics to biology to social science. Yet translating algorithms and ideas into code is no easy task, and mistakes can be costly. A bug in a script can invalidate scientific results, and a bug in a file system can cause catastrophic loss of data. This project makes programming easier for systems programmers and scientists alike, through a novel approach to programming that automates domain-specific languages (DSLs) with solver-aided tools for program verification and synthesis. The intellectual merits are to advance knowledge in programming support for domain-specific verification and synthesis, in co-design of languages and tools, and in applying solver-aided programming to new domains. The project's broader significance and importance are to extend the reach of solver-aided programming by orders of magnitude and to thousands of programmers, facilitating new applications with societal, educational, and industrial impact. The project's key idea is to make verification and synthesis tools, which are usually hand-crafted by computer science PhDs, as simple to build as DSLs, which are developed by a broad spectrum of programmers. The PI's prior work on solver-aided languages has demonstrated that this is possible, enabling a wide range of programmers, from professional developers to high-school students, to rapidly construct synthesis and verification tools for a variety of domains, from radiation therapy software to low-power computing to K-12 education. The resulting tools are based on reduction to Satisfiability Modulo Theories (SMT) solving, and as such, rely on technology that is (1) fundamentally intractable and (2) requires years of experience and training to use effectively. The goal of this proposal is thus to address the central challenge of solver-aided programming: enabling non-experts to diagnose and optimize the performance of solver-aided tools. To achieve this goal, the project develops automatic techniques for (1) symbolic profiling to provide diagnostic information about the causes of scalability bottlenecks across the solver-aided stack; (2) symbolic optimization to mitigate the identified scalability bottlenecks via code refactoring, (meta)sketch mining, and combination of solving engines; and (3) applications to serve as new challenge problems for evaluating symbolic profiling and optimization, and as demos for attracting a diverse population of users, from computer architects to education experts.