BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Coping with Multi-thread Schedules for Detecting Concurrency Bugs
DTSTART:20110622T101500
DTSTAMP:20260406T192434Z
UID:a68a829e9ebbe3fbbca98dfb324f7c883f39dc262f6716f35f8a7ed2
CATEGORIES:Conferences - Seminars
DESCRIPTION:Dr Aarti Gupta\, NEC Laboratories America\nVerification of mul
 ti-threaded programs has to grapple with the core\nproblem of handling an 
 explosive number of thread schedules. In this talk\,I will describe three 
 main approaches we have proposed to cope with this problem\, spanning a ra
 nge of static and dynamic analyses.\n\n- The first is a static analysis fr
 amework for semantic reduction of\nthread interleavings\, where we iterati
 vely refine a transaction graph\nthat captures the interleavings\, by deri
 ving sound invariants using\nabstract interpretation. For data race detect
 ion\, this framework serves\nto reduce the number of false warnings captur
 ed by an initial lockset\nanalysis\, and enables the use of model checking
  on the remaining warnings to generate concrete error traces.\n\n- The sec
 ond approach combines dynamic testing with predictive analysis. Given a te
 st execution of the multi-threaded program\, we derive a symbolic predicti
 ve model to explore all (or some) alternative thread schedules over the sa
 me events\, and use an SMT solver to find violations.\n\n- The third appro
 ach is based on systematic testing\, where we propose a\ncoverage-based me
 tric to choose which interleavings to explore during\nstateless model chec
 king. Although unsound in principle\, the metric works well in practice to
  catch many bugs\, while significantly improving performance in comparison
  to other methods such as dynamic partial order reduction and preemptive c
 ontext bounding. \n Dr Gupta's homepage
LOCATION:BC 01 https://plan.epfl.ch/?room==BC%2001
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR