Reasoning about Java Bart Jacobs bart@cs.kun.nl University of Nijmegen Netherlands

WADT'99

This talk will give an impression of the verification work done in Nijmegen for object-oriented specifications and for Java implementations. The verifications are done with the PVS proof tool, using automatic translations by a special purpose front-end compiler tool. The latter translates classes into logical theories of PVS. The talk will include a demo.

For more information, see http://www.cs.kun.nl/~bart/.