BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Abstract Threads - Alexander Malkis
DTSTART:20091110T130000Z
DTEND:20091110T140000Z
UID:TALK19689@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Verification of large multithreaded programs is challenging. A
 utomatic approaches cannot overcome the state explosion in the number of t
 hreads\; semi-automatic methods require expensive human time for finding g
 lobal inductive invariants. Ideally\, automatic methods should not deal wi
 th the composition of the original threads and a human should not supply a
  global invariant. We provide such an approach. In our approach\, a human 
 supplies a specification of each thread in the program. Here he has the fr
 eedom to ignore or to use the knowledge about the other threads. The check
 s whether specifications of threads are sound as well as whether the compo
 sition of the specifications is error-free are handed over to the off-the-
 shelf verifiers. We show how to apply this divide-and-conquer approach for
  the interleaving semantics with shared variables communication where spec
 ifications are targeted to real-world programmers: a specification of a th
 read is simply another thread. The new approach extends thread-modular rea
 soning by relaxing the structure of the transition relation of a specifica
 tion. We demonstrate the feasibility of our approach by verifying two prot
 ocols governing the teardown of important data structures in Windows devic
 e drivers.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR