Long gone are the days when program veri? cation was a task carried out merely by hand
with paper and pen. For one, we are increasingly interested in proving actual program …

Many state-based specification languages, including the Java Modeling Language (JML),
contain at their core specification constructs familiar to most undergraduates: eg, assertions …

In the last chapter, we explained how the functional behavior of methods can be specified
and verified. Specification of functional method behavior describes the result value and …

Object invariants describe the consistency of object-oriented data structures and are central
to reasoning about the correctness of object-oriented software. Yet, reasoning about object …

Design by Contract, proposed by Meyer for the programming language Eiffel, is a technique
that allows run-time checks of specification violation and their treatment during program …

Classical specification and verification techniques support invariants for individual objects
whose fields are primitive values, but do not allow sound modular reasoning about …

Object invariants define the consistency of objects. They have subtle semantics because of
call-backs, multi-object invariants and subclassing. Several visible-state verification …

This paper presents a logic, called BOTL (Object-Based Temporal Logic), that facilitates the
specification of dynamic and static properties of object-based systems. The logic is based on …

This paper presents the VerCors approach to verification of concurrent software. It first
discusses why verification of concurrent software is important, but also challenging. Then it …

Approaches to runtime checking have to track the execution of a software system and
therefore have to deal with generating and processing execution events. Often these …