Solver-Aided Programming for All

This lecture introduces Solver-Aided Programming, a model integrating SMT solvers into the language to provide constructs for program verification, synthesis, and debugging. It covers topics such as programming with solver-aided tools, localizing bad parts of a program, finding values to repair failing runs, and synthesizing code. The lecture also discusses the challenges of building solver-aided tools and presents ROSETTE, a solver-aided language. It explores the design space of domain-specific languages, the anatomy of solver-aided host languages, and the translation of programs to constraints. Additionally, it delves into type-driven state merging, solver-aided applications in various domains, and strategies for games and education. The lecture concludes with a focus on verifying systems software, including the verification of OS components and the use of Serval verifiers.