KeY, a new tool for the specification and verification of software

Peter Schmitt & Bernhard Beckert

ABSTRACT

The talk will present work in progress. We describe the main features of the KeY specification and verification tool. The discriminating characteristics of the KeY tool are We explain how to use KeY by following a small example.