BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:Undecidability of propositional separation logic a
nd its neighbours - James Brotherston\, Imperial C
ollege London
DTSTART;TZID=Europe/London:20100312T140000
DTEND;TZID=Europe/London:20100312T150000
UID:TALK23542AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/23542
DESCRIPTION:Separation logic has become well-established in re
cent years as\nan effective formalism for reasonin
g about memory-manipulating\nprograms. In this tal
k I shall explain how\, and why\, it happens\nthat
even the purely propositional fragment of separat
ion logic\nis _undecidable_. In fact\, it turns ou
t that all of the\nfollowing properties of proposi
tional separation logic formulas\nare undecidable
(among others):\n\n(a) provability in Boolean BI (
BBI) and its extensions\, even\nwhen negation and
falsum are excluded\;\n\n(b) validity in the class
of separation models\;\n\n(c) validity in the cla
ss of separation models with indivisible\nunits\;\
n\n(d) validity in _any concrete choice_ of heap-l
ike separation\nmodel.\n\nWe also gain new insight
s into the nature of existing\n_decidable_ fragmen
ts of separation logic.\n\nFurthermore\, we additi
onally establish the undecidability of\nthe follow
ing properties of propositional formulas\, which a
re\nrelated to Classical BI and its ''dualising''
resource models:\n\n(e) provability in Classical B
I (CBI) and its extensions\;\n\n(f) validity in th
e class of CBI-models\;\n\n(g) validity in the cla
ss of CBI-models with indivisible units.\n\nAll of
the above results are new but\, in particular\,\n
decidability of BBI has been an open problem for s
ome years\,\nwhile decidability of CBI was a recen
t open problem.\n\nThis is joint work with Max Kan
ovich\, Queen Mary University of\nLondon. The talk
is based on the paper of the same name which\ncan
be found at the speaker's home page:\n\n
http://www.doc.ic.ac.uk/~jbrother\n
LOCATION:Room FW26\, Computer Laboratory\, William Gates Bu
ilding
CONTACT:Sam Staton
END:VEVENT
END:VCALENDAR