BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Static Verification of Concurrent Programs using Reduction and Abs
 traction - Tayfun Elmas - Koc University\, Istanbul
DTSTART:20100429T130000Z
DTEND:20100429T140000Z
UID:TALK24443@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:*Abstract:* Concurrency-related bugs are notoriously difficult
  to discover by code review and testing. By doing a formal proof on the pr
 ogram text\, one can statically verify that no execution of the program le
 ads to an error. The effectiveness of the proof depends on the proper choi
 ce of the manual inputs such as code annotations. Deriving these annotatio
 ns for a concurrent program requires complicated reasoning. The main reaso
 n behind this is the interaction between threads over the shared memory. W
 hile writing the proof\, at every point\, one has to consider the possible
  interleavings of conflicting operations. Existing proof methods including
  Owicki-Gries\, rely/guarantee and concurrent separation logic are applied
  at the finest level of concurrency. Analyzing the program at this level r
 equires complex annotations and invariants\, along with many auxiliary var
 iables.\n\nIn this talk\, we present a new proof method that simplifies ve
 rifying assertions and linearizability in concurrent programs. The key fea
 ture of our method is the use of atomicity as the main proof tool. A proof
  is done by rewriting the program with larger atomic blocks in a number of
  steps. In order to reach the desired level of atomicity\, we alternate pr
 oof steps that apply abstraction and reduction\, each of which improves th
 e outcome of the other in a following step. Then\, we check assertions seq
 uentially within the atomic blocks of the resulting program. We declare th
 e original program correct when we discharge all the assertions. Our proof
  style provides separation of concerns: At each step\, we either use facts
  about a concurrency protocol to enlarge atomic blocks\, or check data pro
 perties sequentially. Our software tool\, QED\, mechanizes proofs using th
 e Z3 SMT solver to check preconditions of the proof steps. We demonstrated
  the simplicity of our proof strategy by verifying well-known programs usi
 ng fine-grained locking and non-blocking data algorithms.\n\nBiography:* T
 ayfun Elmas is a Ph.D. candidate at Koc University (Istanbul\, Turkey)\, a
 dvised by Dr. Serdar Tasiran (Koc Univ.) and Dr. Shaz Qadeer (Microsoft Re
 search). His research interests are formal methods and tools for the debug
 ging\, analysis\, and verification of concurrent software. Tayfun`s recent
  work appeared at premier programming languages conferences (PLDI\, POPL\,
  TACAS)\, workshops (RV\, FATES\, PADTAD)\, and national conferences (UYMS
 \, YKGS). His research is supported by the Scientific and Technological Re
 search Council of Turkey (TUBITAK)\, the Turkish Academy of Sciences (TUBA
 ) and Microsoft Research. The Goldilocks project he primarily involved has
  been selected for publication in SIGPLAN CACM Research Highlights. Tayfun
  was an intern at Microsoft Research (Redmond\,WA) during the summer of 20
 05 and 2007. He received his B.S. in Computer Engineering from Ege Univers
 ity (Izmir\, Turkey) in 2003\, and M.S. in Electrical and Computer Enginee
 ring from Koc University in 2005.
LOCATION:Small public lecture room\, Microsoft Research Ltd\, 7 J J Thomso
 n Avenue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR