Jun 25, 2013: Jelmer ter Wal: JML* specification of selected parts of the Java Collection Framework

June 25, 2013JML* specification of selected parts of the Java Collection Framework
Room: Zi 5126Jelmer ter Wal
12:30-13:30

The Java Collections Framework is part of the backbone of the Java programming language. This talk will describe an on-going MSc-project on an attempt at specifying and verifying parts of this framework using JML* and KeY. JML* is a customized version of JML which makes it easier to do static modular verification. KeY is a standalone prover completely implemented in Java to do verification on dynamic logic derived from JML* annotated Java code.