Abstraction and Refinement for Local Reasoning

Add to your list(s) Download to your calendar using vCal

• Thomas Dinsdale-Young, Imperial College London
• Friday 28 January 2011, 16:00-17:00
• UG40 Computer Science.

If you have a question about this talk, please contact Paul Levy.

Local reasoning has become a well-established technique in program verification, which has been shown to be useful at many different levels of abstraction. In separation logic, we use a low-level abstraction that is close to how the machine sees the program state. In context logic, we work with high-level abstractions that are close to how the clients of modules see the program state. We apply program refinement to local reasoning, demonstrating that high-level local reasoning is sound for module implementations. We consider two approaches: one that preserves the high-level locality at the low level; and one that breaks the high-level `fiction’ of locality.

This is joint work with Philippa Gardner and Mark Wheelhouse, which was presented at VSTTE 2010 .

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• UG40 Computer Science
• computer sience

Note that ex-directory lists are not shown.