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 from Koc University\, Istanbul
DTSTART:20100429T130000Z
DTEND:20100429T140000Z
UID:TALK24719@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. In this talk\, we present a new proof method that simplifies verif
 ying assertions and linearizability in concurrent programs. The key featur
 e 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 st
 eps. In order to reach the desired level of atomicity\, we alternate proof
  steps that apply abstraction and reduction\, each of which improves the o
 utcome of the other in a following step. Then\, we check assertions sequen
 tially within the atomic blocks of the resulting program. We declare the o
 riginal program correct when we discharge all the assertions. Our proof st
 yle provides separation of concerns: At each step\, we either use facts ab
 out a concurrency protocol to enlarge atomic blocks\, or check data proper
 ties sequentially. Our software tool\, QED\, mechanizes proofs using the Z
 3 SMT solver to check preconditions of the proof steps. We demonstrated th
 e simplicity of our proof strategy by verifying well-known programs using 
 fine-grained locking and non-blocking data algorithms. \n\n*Biography:* Ta
 yfun Elmas is a Ph.D. candidate at Koc University (Istanbul\, Turkey)\, ad
 vised by Dr. Serdar Tasiran (Koc Univ.) and Dr. Shaz Qadeer (Microsoft Res
 earch). His research interests are formal methods and tools for the debugg
 ing\, 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 Res
 earch 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 200
 5 and 2007. He received his B.S. in Computer Engineering from Ege Universi
 ty (Izmir\, Turkey) in 2003\, and M.S. in Electrical and Computer Engineer
 ing from Koc University in 2005. \n
LOCATION:Small public lecture room\, Microsoft Research Ltd\, 7 J J Thomso
 n Avenue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR