Copenhagen Programming Language Seminar
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.
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 email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org