JetBrains Research unites scientists working in challenging new disciplines

Seminar: Structuring the Synthesis of Heap-Manipulating Programs

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

30.09.2019, 17:15.

Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg

State University, Stary Peterhof, Universitetski pr., 28