Tutorial on Deductive Program Synthesis - Part 2: Hands-on Derivation and Advanced Techniques

Dive into the inner workings of deductive program synthesis in this 42-minute tutorial, the second part of a series focusing on the SuSLik system for creating provably correct pointer-manipulating programs. Explore synthetic separation logic (SSL) and its basic rules through hands-on examples like swapping elements and managing bank accounts. Tackle challenging tasks such as tree flattening, learning how to handle recursion and utilize cyclic proofs. Gain practical experience in deriving programs from specifications step-by-step using deductive rules, and understand the fundamental idea behind deductive synthesis: finding the program by looking for the proof.

this tutorial
synthetic separation logic (SSL)
SSL: basic rules
example: swap
demo: bank account
deposit
demo: deriving dispose
deriving single-to-double
example: tree flattening
this task is challenging!
tree flattening with cyclic proofs
does this goal look familiar?
extracting the auxiliary
deductive synthesis idea: to find the program, look for the proof