dar seminar - Scott Stoller: Checking Java Programs ...

		 Design and Analysis Research Seminar
                         Wed., Oct. 24, 2001
                     2-3pm, CS Seminar Room 1306

			 Checking Java Programs
	    for Concurrent, Distributed, Open, Secure Systems

			    Scott Stoller

This talk summarizes recent work whose immediate goal is to enable
checking of Java programs by state-space exploration.  Most of the
techniques are applicable to other languages and other verification
methods as well.  Major techniques include reducing the number of
interleavings and states explored for concurrent systems that use locks
and condition variables, transforming distributed systems into
centralized systems that can be handled by existing model checkers for
Java, generating environments for open systems, generating attackers for
secure systems, and simulating cryptographic operations during checking
of secure systems.

The plan for the rest of the talks of this semester, in order, is:
Amir Pnueli (NYU and Weizmann), Radu Grosu, Ziyang Duan and Art
Bernstein, Michael Kifer, John Field (IBM Watson), IV Ramakrishnan.