Synthesis of Safe Pointer-Manipulating Programs

This lecture by the instructor focuses on the synthesis of safe low-level pointer-manipulating programs using program synthesis technology. The talk introduces SuSLik, a program synthesizer that generates provably safe C programs from logical specifications, showcasing its capabilities in handling linked data structures. The lecture covers deductive synthesis of pointer-manipulating programs, the use of separation logic, and the application of synthetic separation logic in deriving correct-by-construction programs. Examples such as swapping values of pointers and disposing of lists are demonstrated, emphasizing the importance of correct program synthesis in eliminating memory safety bugs.