[Brown CS Talks] Brown CS Seminar: Shaz Qadeer in Lubrano on 4/16/02 at noon

[talks-admin@list.cs.brown.edu]

			      CS Seminar
		  
		  The Department of Computer Science
			   BROWN UNIVERSITY

			      
			       presents

			     Shaz Qadeer

		     Compaq Computer Corporation

		   Tuesday, April 16, 2002 at noon
	       Lubrano Conference Room (CIT 4th floor)
	       Refreshments will be served at 11:45 am
			       
		      
	    Formal Analysis of Concurrent Computer Systems
 

			       Abstract

Computer systems are increasing in complexity.  Moreover, these
systems are being deployed in mission-critical situations where
failure has catastrophic consequences.  Therefore it is imperative to
provide designers of such systems with analysis tools.  These tools
must reason formally about complex systems and detect design errors
before deployment.  Concurrency is a feature of modern computer
systems that is particularly difficult to reason about.  It is present
at all levels of abstraction from microprocessors to systems programs
(OS and databases) to multithreaded and distributed applications.  I
will present my recent work on formal analysis of complex concurrent
systems using model checking and automated theorem proving techniques.

In the first part of the talk, I will describe Calvin, a tool which
checks multithreaded programs for synchronization errors and invariant
violations.  Calvin has been used to check synchronization-rich parts
of the Mercator web crawler, which has been in production use at
Altavista for the past several years.  In the second part of the talk,
I will describe a technique to verify that a cache-coherence protocol
implements sequential consistency.  Although this problem is
undecidable in the general case, properties of cache-coherence
protocols occuring in practice allow automatic verification using
model checking techniques.


		     Host:  Professor Steve Reiss