Satisfiability-based Program Reasoning and Synthesis

Опубликовано 17 августа 2016, 21:05

Today, software is ubiquitous---it is deployed on virtually all electronic devices, small and large, including those that are life- and safety-critical. The need for robust, certifiably correct software requires us to develop the theory and tools for mechanically reasoning about, and also automatically generating, programs. In this talk, I will present the theory and practice behind a novel approach to program reasoning and program synthesis. Program reasoning is the task of verifying a program against its specification, and of inferring the specification given a program. Program synthesis is the task of automatically generating the program corresponding to a specification. I will describe novel algorithms that reduce program reasoning and synthesis to SAT/SMT solving problems, which permits leveraging the substantial engineering advances present in today's solvers. Our tools based on this theory can reason about expressive properties of programs, e.g., quantified properties, that were beyond the reach of previous techniques. Leveraging program reasoning, we will describe how we can automatically synthesize programs from specifications, e.g., sorting programs and Strassen's matrix multiplication, which was not possible earlier.