DIKU IT-C RUC

COPLAS

Copenhagen Programming Language Seminar


Modular verification of object invariants in Spec#

Peter Müller
ETH Zürich

Thursday, March 15th, Time: 15:15 - 16:00
IT University of Copenhagen, Rued Langgaards Vej 7, auditorium 3

Abstract:

The talk describes a methodology for specifying and verifying object-oriented programs, using object invariants to specify the consistency of data, using ownership to organize objects into dynamic contexts, and using visibility to verify programs that escape an ownership structure. The methodology is designed to allow modular reasoning, even in the presence of subclasses and callbacks.


Scientific host: Lars Birkedal. Administrative host: Camilla Torp-Smith. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC. COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body. For more information about COPLAS, see http://www.coplas.org