Lecture

Synthesis of Safe Pointer-Manipulating Programs

Description

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.

About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.