Formalising Java Safety

Pieter H. Hartel

Dept. of Electronics and Computer Science
University of Southampton
phh@ecs.soton.ac.uk

We review the existing literature on Java safety, emphasizing formal approaches, and the impact of Java safety on small footprint devices such as smart cards. The conclusion is that while a lot of good work has been done, a more concerted effort is needed to build a coherent set of machine readable formal models of the whole of Java and its implementation. This is a formidable task but we believe it is essential to building trust in Java safety.

Pieter Hartel received an MSc in Mathematics from the Free University in Amsterdam and a PhD in Computer Science from the University of Amsterdam. He has worked at CERN in Geneva and the Universities of Nijmegen and Amsterdam. He came to Southampton in 1995, where he is a Senior Lecturer. Dr Hartel consults for IT companies in the USA and in Europe. He has over 75 publications in the areas of programming languages, smart cards and formal methods, he is chair and founding member of the IFIP working group 8.8 on smart cards, and he has served on dozens of international programme committees.