BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Stateless Model Checking with Data-Race Preemption Points (Systems
  Seminar by Ben Blum\, CMU)
DTSTART:20161107T141500
DTEND:20161107T150000
DTSTAMP:20260408T071148Z
UID:aca5388a95de74cf4a43aa0c85e15ab165bab5f1493bdd1bb38b19d1
CATEGORIES:Conferences - Seminars
DESCRIPTION:Ben Blum\, CMU\nAbstract: Stateless model checking is a power
 ful technique for testing concurrent programs\, but suffers from exponenti
 al state space explosion when the test input parameters are too large. Dat
 a race detection\, another concurrency testing approach\, focuses on suspi
 cious memory access pairs during a single test execution. It avoids concer
 ns of state space size\, but may report races that do not lead to observab
 le failures\, which jeopardizes a user’s willingness to use the analysis
 .\n\nQuicksand is a new stateless model checking framework which manages t
 he exploration of many state spaces using different preemption points. It 
 uses state space estimation to prioritize jobs dynamically\, and incorpora
 tes data-race analysis to add new preemption points on the fly. Preempting
  during racy instructions can automatically classify the race as buggy or 
 benign\, and also enables full verification of all possible schedules when
  completion is possible within the CPU budget. In our evaluation\, Quicksa
 nd found 1.25x as many bugs and verified 4.3x as many tests compared to pr
 ior model checking approaches.\n\nBio: Ben Blum is a graduate student in 
 the Computer Science Department at Carnegie Mellon (CMU)\, advised by Gar
 th Gibson. Before starting his PhD\, he worked on Landslide\, a tool to sy
 stematically test software under all possible thread interleavings.\n\nCof
 fee will be available 15 minutes before the talk.
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR