Speaker: Christoph Gladisch, University of Koblenz-Landau

Title: Verification and Testing with KeY

Abstract: The KeY tool is a semi-automatic software verification and
test generation tool for JavaCard. KeY is a powerful tool as it can
reason about arbitrary data structures expressible in first-order logic.
In this talk the  dynamic logic and sequent calculus of the verification
tool will be presented which build the foundations of the tool. The
verification and test generation process will presented as a demo and
selected techniques of the tool will be discussed.