Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities

This paper presents the main ideas behind deductive synthesis of heap-manipulating program and outlines present challenges faced by this approach as well as future opportunities for its applications.