

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

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

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 heaplike models of practical interest.
2. Inplace 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 heaplike 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 nontrivial $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 ‘pointsto’ predicate, and an inductive predicate
for describing linkedlist segments. Standard entailment turns out to be decidable in polytime, while abduction ranges from NPcomplete to polytime for different subproblems. The following parametrized
complexity is of great practical and theoretical importance — that is, the NPcompleteness 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

