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.

Intro
follow along
we've come a long way...
program synthesis with guarantees
this tutorial
example: swap
demo: swap
exercise 1: rotate three
separation logic (SL)
programs
SL assertions
example triples
example: dispose
dynamic data structures
the linked list predicate
demo: dispose a list
example: copy
linked list with elements
demo: copy a list
exercise 2: single to double