BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Nitpicking C++ Concurrency - Jasmin Blanchette - TU München
DTSTART:20110707T100000Z
DTEND:20110707T110000Z
UID:TALK32029@talks.cam.ac.uk
CONTACT:Tjark Weber
DESCRIPTION:Previous work formalized the C++ memory model in Isabelle/HOL 
 in an\neffort to clarify the proposed standard's semantics. Here we employ
  the\nmodel finder Nitpick to check litmus test programs that exercise the
 \nmemory model\, including a simple locking algorithm. Nitpick is built on
 \nKodkod (Alloy's backend) but understands Isabelle's richer logic\; hence
 \nit can be applied directly to the C++ memory model. We only need to\ngiv
 e it a few hints\, and thanks to the underlying SAT solver it scales\nmuch
  better than the Cppmem explicit-state model checker. This case\nstudy ins
 pired optimizations in Nitpick from which other formalizations\ncan now be
 nefit.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR