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.