|
|
|
|
Copenhagen Programming Language SeminarCOPLAS Talk |
|
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