BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Effective Stateless Model Checking for C/C++ Concurrency - Viktor 
 Vafeiadis\, MPI-SWS
DTSTART:20171205T103000Z
DTEND:20171205T113000Z
UID:TALK96466@talks.cam.ac.uk
CONTACT:Victor Gomes
DESCRIPTION:I will present a stateless model checking algorithm for verify
 ing concurrent programs running under RC11\, a repaired version of the C/C
 ++11 memory model without dependency cycles. Unlike previous approaches\, 
 which enumerate thread interleavings up to some partial order reduction im
 provements\, our approach works directly on execution graphs and (in the a
 bsence of RMW instructions and SC atomics) avoids redundant exploration by
  construction.  We have implemented a model checker\, called RCMC\, based 
 on this approach and applied it to a number of concurrent programs. Our ex
 periments confirm that RCMC is significantly faster\, scales better than o
 ther model checking tools for sequential consistency\, and is also more re
 silient to small changes in the benchmarks.\n\n(This is joint work with Mi
 chalis Kokologiannakis\, Ori Lahav\, and Konstantinos Sagonas\, and will a
 ppear at POPL'18.)
LOCATION:FW26
END:VEVENT
END:VCALENDAR