[pl-seminar] Talk Reminder

[Nick Kidd <kidd@xxxxxxxxxxx>]

4:00 pm, 3310
Programming Languages Seminar: Nicholas Kidd, University of   
Wisconsin,  "Model
   Checking Concurrent C Programs"
   85%  of  the  system  crashes  in  Windows  XP  are caused by  
bugs in device
   drivers. Because of the difficultly involved with kernel  
programming, better
   static analysis tools are needed for program verification. Better  
tools will
   catch bugs earlier in the development cycle which in turn can  
save thousands
   of  dollars  in development costs. To this end, we have developed  
a tool for
   model checking concurrent C programs. Our tool is able to  
handle:  (1)  data
   ranging  over  very  large domains, (2) (recursive) procedure  
calls, and (3)
   concurrent parallel components that communicate via   
synchronizing  actions.
   We  model such programs using communicating pushdown systems, and  
reduce the
   reachability problem for this model to deciding the emptiness of  
the  inter-
   section  of two context-free languages L1 and L2. We tackle this  
undecidable
   problem using a CounterExample Guided Abstraction Refinement  
(CEGAR) scheme.
   Our  tool  is  implemented in the model checker MAGIC and found a  
previously
   unknown bug in a model of a Windows NT Bluetooth driver. This is  
joint  work
   with Sagar Chaki, Edmund Clarke, Thomas Reps, and Tayssir Touili.