DIKU ITU KVL

Copenhagen Programming Language Seminar

COPLAS Talk

Extending over-approximating models: an introduction to mixed models and separation logic

David Schmidt,
Computing and Information Sciences Dept., Kansas State University

Thursday, March 18, 15:15-16:00
DIKU, Universitetsparken 1, room N010

Abstract:

Programs, communicating processes, and storage heaps are often modelled by graphs, which are formalized by over-approximating relations. Then, correctness properties are validated on the models. It is well known that universal (but not existential) properties can be safely validated on over-approximating models.

In this presentation, we review over-approximating models and their specification logic. Then, we consider two approaches for enriching the model and logic for validating existential properties:

1) adding under-approximating relations to the model (the result is a "mixed model", due to Dams and Larsen);
2) adding a "separation operator" to the logic (the result is a "separation logic", due to Reynolds and O'Hearn).

The presentation introduces mixed models and separation logic and explains why they are useful for modelling and validation.

Scientific host: Fritz Henglein. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
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