Lightweight Assertion Checking; or, Towards Safe Fundamental Code

Advanced Programming Specialist Group event

Thursday 13 February 2003, 6.00pm

Sun Microsystems office, Regis House, 45 King William Street, London EC4. The nearest underground stations are Cannon Street and Bank.

Professor Peter O'Hearn, Queen Mary & Westfield College, London


Reasoning about programs has always been a fundamental concern in computer science. Recently, there as been renewed interest in this subject, in industry as well as in academe, and several impressive tools for automatic reasoning about programs have emerged. Surprisingly, these tools work not on cleaned-up "toy" programs, but often on realistic, legacy code written in C.

We outline the technology behind some of the recent developments, particularly on software model checking. Then, more specifically, we describe a novel approach to reasoning about low-level pointer data structures, and we describe a prototype tool for reasoning with the logic.

We discuss the prospects for having a mechanized form of lightweight assertion checking, which provides for the fundamental code in a system safety guarantees analogous to those provided by types in high-level languages.

Free, but for security purposes, please send your name to the Vice-Chairman at [This registration is needed for each individual meeting]

CPD Value:
Half unit