Department of Computer Science Colloquium
4:15pm, October 18th, 2001
B17 Upson Hall
Extended Static Checking for Java
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
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.