Популярное видео

Новые поступления

Для просмотра файлов Вам могут потребоваться

Международная конференция «Logical Models of Reasoning and Computation»
2 февраля 2012 г. 10:45, г. Москва, МИАН

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

Max Kanovich

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

Количество просмотров:
Эта страница:265

Max Kanovich

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

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

Аннотация: 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$.

Язык доклада: английский

ОТПРАВИТЬ: FaceBook Twitter Livejournal
Обратная связь:
 Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2017