BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Linear maps - David Walker (visiting from Princeton)
DTSTART:20100628T114500Z
DTEND:20100628T130000Z
UID:TALK25384@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:Over the last decade\, separation logic has risen to the top o
 f the\ncharts.  When I arrived at Microsoft Research Redmond last fall for
  a\nsabbatical from Princeton\, Shaz Qadeer and Shuvendu Lahiri ask why?\n
 Why are so many researchers so excited about this new advance?  And\,\nthe
 y asked\, *can we get what they've got*?\n\nThese questions led us to try 
 to capture the spirit of the separation\nlogic proof strategy in a classic
 al first-order theorem proving\nenvironment.  To be more specific\, we sou
 ght a conservative extension\nof Boogie\, which is a classical verificatio
 n condition generator for\nimperative programs\, that would admit the use 
 of effective frame and\nanti-frame rules and thereby allow the kinds of mo
 dular proofs that\nmake separation logic so attractive.  However\, we did 
 not want to have\nto change the underlying theorem proving technology\, so
  any\nverification conditions generated would have to be ordinary\nfirst-o
 rder logic formulae over terms from well supported theories\nsuch as the t
 heories of arrays\, sets and arithmetic.  Moreover\, in\norder for our the
 orem prover\, Z3\, to be able to discharge the\nverification conditions ef
 fectively\, it was essential that they\ncontain no more quantifiers than n
 ormal.\n\nIn this informal whiteboard talk\, I will explain our solution t
 o the\nproblem\, which is to add a new data type called a "linear map" to\
 nBoogie.  Linear maps seem to have a number of very nice properties:\n\n *
  the ideas are simple: I hope means other researchers will have an\n   eas
 y time building on them.\n\n * verification conditions for operations on l
 inear maps can be\n   expressed in first-order logic using the theories of
  arrays\, sets\n   and arithmetic\n\n * they work: we have used Boogie\, Z
 3 and linear maps to mechanically\n   verify classic examples drawn from p
 ast papers on separation\n   logic.\n\nIf you want to find out what linear
  maps actually are\, you'll have to\ncome to the talk!\n
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR