Chair of Software Engineering

Proving Program Pointer Properties
Bertrand Meyer

Work In Progress



This series of four articles, currently in draft form, provides a general model for reasoning about the properties of run-time structures involving references (pointers) between objects.

The articles (all PDF) are the following:

The last article is not yet available in the same form as the others parts, but the results so far are covered in a self-contained article written to be readable independently of the rest: Towards practical proofs of class correctness. (Revision: 17 February 2003)


Meyer home  -   Publications  -   Events  -  Software engineering home  -   CS home