The LOOP project: Formal methods for object-oriented systems

LOOP stands for Logic of Object-Oriented Programming. It is the name of a research project, and also the name of the tool that plays a central role in this project. The topic is formal methods for object-oriented languages. The aim is to specify and verify properties of classes in object-oriented languages, using proof tools like PVS and Isabelle, but also static checkers like ESC/Java.

There is a fruitful interaction between theory and practice within the LOOP project. The theoretical basis is formed by so-called coalgebras, which are used for the semantics of Java, leading to verifications of actual Java programs, and also for the semantics of the annotation language JML for Java. Our main focus of application is JavaCard, a stripped down version of Java for programming the latest generation of smart cards. One of the main challenges that we see in this area is to bridge the gap between high level security properties and low level program properties.

The LOOP group is coordinator of a European project VerifiCard in this area. It also runs several national projects related to smart cards.