|
Dr. K. Rustan M. Leino
Compaq SRC, Palo Alto, CA Monday , May 7th, 22 Schaeffer Hall, 10:30 am - 11:20 am |
ABSTRACT:
ESC/Java is a static program checker for Java, powered by a detailed semantics engine and an automatic theorem prover. It performs modular checking and relies on the programmer to supply light-weight specifications. Houdini is a programming tool built on top of ESC/Java. By inferring many properties of the program, it can be useful as a program checker even in the absence of programmer-supplied specifications. This talk gives an overview of ESC/Java and Houdini and reports on some initial experience with Houdini. (Joint work with Cormac Flanagan.)
Dr. Rustan Leino is
a computer science researcher at Compaq SRC, he
has worked mostly in programming languages, systems, and
semantics. For example, he led the Extended Static Checking
for Java (ESC/Java) project, and is currently heading up
a Software Quality Assurance effort that includes the Houdini
tool. 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/