REASONING AND PROGRAM SYNTHESIS

Program reasoning consists of the tasks of automatically and statically ver-ifying correctness and inferring properties of programs. Program synthesis is the task of automatically generating programs. Both program reasoning and synthesis are theoretically undecidable, but the results in this dissertation show that they are practically tractable. We show that there is enough structure in programs written by human developers to make program reasoning feasible, and additionally we can leverage program reasoning technology for automatic program synthesis. This dissertation describes expressive and efficient techniques for program rea-soning and program synthesis. Our techniques work by encoding the underlying inference tasks as solutions to satisfiability instances. A core ingredient in the re-duction of these problems to finite satisfiability instances is the assumption of tem-plates. Templates are user-provided hints about the structural form of the desired artifact, e.g., invariant, pre- and postcondition templates for reasoning; or program templates for synthesis. We propose novel algorithms, parameterized by suitable templates, that reduce the inference of these artifacts to satisfiability