Designing concurrent programs is difficult. The nondeterministic interaction between concurrently executing threads of a concurrent program results in programming errors that are notoriously difficult to reproduce and fix.  Shaz Qadeer of Microsoft presents a new static analysis technique based on model checking for automatically finding errors in concurrent software. An execution of a concurrent program is a sequence of contexts, where each context consists of transitions performed by a single thread. KISS (Keep It Simple and Sequential), is a technique for transforming a concurrent program P into a sequential program Q that encodes all executions of P with a small number of contexts. KISS is used to convert SDV (Static Driver Verifier), a model checker for sequential C programs, into a model checker for concurrent C programs. The combination of KISS and SDV has been used to find a number of subtle concurrency errors in Windows device drivers. From the Series:CSE Colloquia - 2005