Slides from the talk [pdf]
Abstract: A great deal of computer program errors arise due to the human programmer dealing with error-prone low-level details. Automated synthesis of computer programs could exempt programmers from this tedious task by generating correct-by-construction solutions according to the requirements provided. A recently-published technique encodes program synthesis problems as program verification problems solvable by appropriate high-end verification tools. In comparison with previous approaches the novelty of this technique lies in that it synthesizes a proof of correctness for the result alongside the required program itself. In this talk we concentrate on this late technique, appropriately named proof-theoretic synthesis, and present experimental results.
Main references: