Nadia Polikarpova (UCSD)/Shachar Itzhaky (Technion)

This tutorial is an introduction to deductive program synthesis, using as an example synthesis of provably correct pointer-manipulating programs with the SuSLik system.

In the second part of the tutorial, we will see how deductive synthesis works under the hood. We will get hands-on experience deriving programs from specifications step-by-step using deductive rules and explore how deductive synthesis handles recursion.