On the Role of Invariants in Reasoning about Object-Oriented Languages (2008)
Cees-bart Breunesse, Bart Jacobs, Erik Poll
1 Introduction Preconditions, postconditions and invariants are universally accepted as the basic ingredients for specification of OO programs. Invariants for classes play an important role in...
with contributions from (2008)
Joseph R. Kiniry, Patrice Chalin, Clément Hurlin, Cees-bart Breunesse, Julien Charles, ...
Automatic verification by means of extended static checking (ESC) has seen some success in industry and academia due to its lightweight and easy-to-use nature. Unfortunately, ESC comes at a cost: a...
with contributions from (2008)
Joseph R. Kiniry, Patrice Chalin, Clément Hurlin, Cees-bart Breunesse, David Cok, ...
Automatic verification by means of extended static checking (ESC) has seen some success in industry and academia due to its lightweight and easy-to-use nature. Unfortunately, ESC comes at a cost: a...
On the Role of Invariants in Reasoning about Object-Oriented Languages (2007)
Cees-Bart Breunesse, Bart Jacobs, Erik Poll
The aim of this paper is to clarify the di#erent roles that class invariants play in the verification of object-oriented programs, namely in method specifications as proof obligations for method...
Verifying JML specifications with model fields (2003)
Cees-bart Breunesse, Erik Poll
Abstract. The specification language JML (Java Modeling Language) provides model fields as a means to abstract away from implementation details in specifications. This paper investigates how...
Specifying and verifying a decimal representation in Java for smart cards (2002)
Cees-bart Breunesse, Bart Jacobs
Abstract. This article describes a case study concerning a component of a Java Purse applet developed by the smart card manufacturer Gemplus. This component is a representation of decimal numbers in...
Voting using Java Card smart cards: A case study (2002)
Cees-Bart Breunesse, Bart Jacobs, Martijn Oostdijk
This paper documents a case study in the development of a Java Card application and describes some related security issues. An implementation of a simpli ed electronic voting system is presented, in...
Specifying and verifying a decimal representation in Java for smart cards (2002)
Cees-bart Breunesse, Bart Jacobs
Abstract. This article describes a case study concerning a component of a Java Purse applet developed by the smart card manufacturer Gemplus. This component is a representation of decimal numbers in...