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

Photo Gallery

 Видео не загружается в Ваш браузер: Активируйте JavaScript в Вашем браузере Установите Adobe Flash Player     Проверьте с Вашим администратором, что из Вашей сети разрешены исходящие соединения на порт 8080 Сообщите администратору портала о данной ошибке

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: