JetBrains Research — наука, меняющая мир

Семинар: Синтез императивных программ, использующих кучу

Аннотация:

Темой доклада является дедуктивный подход к синтезу императивных программ с указателями по декларативной спецификации, выраженной в логике разделения (расширении логики Хоара). Декларативная спецификация представляет из себя пару утверждений - предусловие и постусловие - которые описывают состояния кучи до и после исполнения синтезируемой программы.

В ходе доклада мы обсудим систему синтеза императивных программ, представленную в виде набора правил вывода, а также рассмотрим несколько вопросов реализации этой системы.

Докладчик --- Петр Лозов

30.09.2019, 17:15.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 28