Cornell Department of Computer Science Colloquium
4:15pm, October 18th, 2001
B17 Upson Hall

Extended Static Checking for Java

Rustan Leino
Compaq Corporation

The Extended Static Checker for Java (ESC/Java) is a programming tool for finding, at compile-time, common programming errors that usually are not found until run-time, and sometimes not even then. The tool is powered by program verification technology, but feels to a user more like a type checker. To use it, a programmer annotates the program with simple specifications.  In this talk, I will give an overview of the system, give a short demo, discuss our experience in using the checker on real Java programs, and outline on some future directions. Joint work with Cormac Flanagan, Mark Lillibridge, Greg Nelson, Jim Saxe, and Raymie Stata.

For more information, please go to:  http://research.compaq.com/SRC/esc

Brief Bio:

A computer science researcher at Compaq SRC, Rustan Leino has worked mostly in programming languages, systems, and semantics. For example, he led the Extended Static Checking for Java (ESC/Java) project, and worked on a follow-on tool called Houdini. Leino received his PhD and MS in Computer Science from Caltech in 1995 and 1993, respectively. Before entering the graduate program at Caltech in 1991, he was a technical lead in the Windows/NT group at Microsoft. In 1989, he received his BA with Special Honors in Computer Science from UT Austin. Leino lives with his wife and their four children in Sunnyvale, CA.

http://research.compaq.com/SRC/personal/rustan
http://leino-online.com/rustan