Formal Methods in the Software Life Cycle

[ main | background | applications | schedule | deliverables ]

Goals

The aim of this OOTI course is to do some fun programming using Java Card smart cards, and to use a variety of state-of-the-art techniques for formal specification and analysis, both for the security protocols that will be implemented using smart cards, and for the Java (Card) source code of the actual implementations.

More background information on the languages, methods, and tools, and the hardware that you will be using is available.

Lecturers

The course is taught by Erik de Vink from Eindhoven University of Technology, and Engelbert Hubbers, Joe Kiniry, Martijn Oostdijk, and Erik Poll from the SoS group at the University of Nijmegen.

Organisation

In groups of 4 or 5 people you will develop a Java (Card) application that uses smart cards; As part of the development process some techniques for formal specification and analysis will be applied. The applications will be made to run on actual smart cards. There are four applications for the groups to choose from.

Weekly lectures, usually on Mondays, introduce the required background knowledge for the languages, methods, and tools to be used.

A detailed schedule (including slides of presentations) is available. More information, e.g. about the assignments etc., will be made available in due course.