Correctness of Java programs Brightsight congratulates Joachim van den Berg with being awarded his Ph.D. degree on Thursday July 2, 2009. Joachim defended his thesis "Reasoning about Java programs in PVS using JML" at the Institute for Computing and Information Sciences of the Radboud University Nijmegen, The Netherlands.

The thesis of Joachim concerns program verification and especially verification of Java Card platforms and Java Card applications. Joachim made a connection between theoretical knowledge and practical applicability in the smart card industry. He formalised the semantics of the specification language JML (Java Modeling Language). This semantics is used to prove correctness of Java programs. Joachim's work has been validated in two case studies

Verification of programs is also of importance in the assessment of security. Many of today's smart cards are based upon Java technology. The structured approach proposed by Joachim enables Brightsight to improve their security assessments as well. Furthermore, the higher assurance levels of the Common Criteria for IT Security Evaluation require formal methods to proof correctness and completeness of security designs. Other evaluation methodologies also will use this type of verification more and more.

Joachim is a senior evaluator in Brightsight. He is involved in the assessment of the quality of security in smart cards and related systems against state-of-the-art attacks. Joachim represents Brightsight in the JHAS group. For more information please contact berg@brightsight.com or info@brightsight.com