RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PERSONAL OFFICE
Video Library
Archive
Most viewed videos

Search
RSS
New in collection





You may need the following programs to see the files






International workshop "Logical Models of Reasoning and Computation"
February 2, 2012 10:45, Moscow, Steklov Mathematical Institute
 


How and Why Separation Logic is good for Resource Reasoning about Programs

Max Kanovich

University of London
Video records:
Flash Video 2,187.9 Mb
Flash Video 359.8 Mb

Number of views:
This page:247
Video files:90

Max Kanovich
Photo Gallery


Видео не загружается в Ваш браузер:
  1. Установите Adobe Flash Player    

  2. Проверьте с Вашим администратором, что из Вашей сети разрешены исходящие соединения на порт 8080
  3. Сообщите администратору портала о данной ошибке

Abstract: Separation logic, invented by John C. Reynolds and Peter O'Hearn, has proven to be an effective formalism for the analysis of programs that manipulate memory (in the form of pointers, heaps, stacks, etc.). In addition to the standard propositional connectives, the most important feature of separation logic is its separating conjunction ($A*B$) which holds for a portion of memory, a heap $h$, iff $h$ can be split into separate $h_1$ and $h_2$ so that $A$ holds for $h_1$ and $B$ holds for $h_2$.
In my talk I will address the following issues.
1. General separation models, and concrete heap-like models of practical interest.
2. In-place reasoning, the frame property, the weakest preconditions, inductive definitions (linked lists, trees), within separation logic used as an extension of Hoare logic.
3. As for the assertion language of separation logic, even purely propositional separation logic turns out to be undecidable. What is more, whatever concrete heap-like model $H$ we take, it is undecidable whether a purely propositional formula $A$ is valid in this model $H$. A number of propositional systems which approximate separation logic are undecidable as well. In particular, these include both Boolean BI and Classical BI. Oddly enough, Intuitionistic BI is still decidable.
4. Abduction, the problem of discovering hypotheses that support a conclusion, has mainly been studied in the context of philosophical logic and AI. Recently, the abduction principle — given $A$ and $B$, find a non-trivial $X$ such that $A*X$ entails $B$, is one of the powerful practical tools for iterated deduction and hypothesis formation to ‘dig information out of bare code’. We study the complexity of abduction for a relevant fragment of separation logic over ‘symbolic heaps’ which include a basic ‘points-to’ predicate, and an inductive predicate for describing linked-list segments. Standard entailment turns out to be decidable in polytime, while abduction ranges from NP-complete to polytime for different sub-problems. The following parametrized complexity is of great practical and theoretical importance — that is, the NP-completeness notwithstanding, there is a polytime procedure for finding a solution to abduction but degree of the polynomial is proportional to the number of ‘list segment’ subformulas in $B$.

Language: English

SHARE: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru
 
Contact us:
 Terms of Use  Registration  Logotypes © Steklov Mathematical Institute RAS, 2017