line

ESC/Java and Houdini

K. Rustan M. Leino
Compaq Systems Research Center
Palo Alto, U.S.A.

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. (Houdini is joint work with Cormac Flanagan.)


ASTEC seminar
May 29, 2001

Place: Information technology, Uppsala University
Room: 1113
Time: 15.15-16.00 (+ discussions)

Room 1113 is in building 1, floor 1, room 13 (in the southern part of the building).

Help on how to find ASTEC Seminars.

There will be an extended period for discussions after the seminar.

Speakers are encouraged to give an short (5 min) introduction to the subject at the begining of the talk.
Listeners are excused if they have to leave after 16.00.

Everyone is welcome !

line
Updated 14-May-2001 14:43 by Roland Grönroos
e-mail: info -at- astec.uu.se    Location: http://www.astec.uu.se/Seminars/01/0529.shtml