SuSLik: Deductive Synthesis of Safe Programs with Pointers - Tutorial 1b

Explore deductive program synthesis through an introduction to the SuSLik system, focusing on creating provably correct pointer-manipulating programs. Delve into the motivation and core concepts of deductive synthesis, practicing program specification using formal logic. Learn about separation logic (SL) and its application to programs, including SL assertions and example triples. Examine dynamic data structures, with a particular emphasis on linked lists. Engage in hands-on exercises, such as rotating three elements and converting a singly linked list to a doubly linked list. Follow along with demonstrations on swapping elements, disposing of lists, and copying linked lists, gaining practical insights into synthesizing safe programs with pointers.