BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Undecidability of propositional separation logic and its neighbour
 s - James Brotherston\, Imperial College London
DTSTART:20100312T140000Z
DTEND:20100312T150000Z
UID:TALK23542@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:Separation logic has become well-established in recent years a
 s\nan effective formalism for reasoning about memory-manipulating\nprogram
 s. In this talk I shall explain how\, and why\, it happens\nthat even the 
 purely propositional fragment of separation logic\nis _undecidable_. In fa
 ct\, it turns out that all of the\nfollowing properties of propositional s
 eparation logic formulas\nare undecidable (among others):\n\n(a) provabili
 ty 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 class of separation models with indivisible\nunits\;\n\n(
 d) validity in _any concrete choice_ of heap-like separation\nmodel.\n\nWe
  also gain new insights into the nature of existing\n_decidable_ fragments
  of separation logic.\n\nFurthermore\, we additionally establish the undec
 idability of\nthe following properties of propositional formulas\, which a
 re\nrelated to Classical BI and its ''dualising'' resource models:\n\n(e) 
 provability in Classical BI (CBI) and its extensions\;\n\n(f) validity in 
 the class of CBI-models\;\n\n(g) validity in the class of CBI-models with 
 indivisible units.\n\nAll of the above results are new but\, in particular
 \,\ndecidability of BBI has been an open problem for some years\,\nwhile d
 ecidability of CBI was a recent open problem.\n\nThis is joint work with M
 ax Kanovich\, Queen Mary University of\nLondon. The talk is based on the p
 aper 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 Building
END:VEVENT
END:VCALENDAR