The topic of the talk is a deductive approach to the synthesis of imperative programs with pointers from the declarative specification expressed in the separation logic (extension of the Hoar logic). The declarative specification is a pair of statements - a precondition and a postcondition - which describe the state of the heap before and after the execution of the synthesized program. In the talk, we will discuss the synthesis system of imperative programs, presented in the form of a set of inference rules, and also consider several issues of the implementation of this system.
Presenter: Petr Lozov
State University, Stary Peterhof, Universitetski pr., 28