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.