University of Birmingham > Talks@bham > Theoretical computer science seminar > Abstraction and Refinement for Local Reasoning

Abstraction and Refinement for Local Reasoning

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

  • UserThomas Dinsdale-Young, Imperial College London
  • ClockFriday 28 January 2011, 16:00-17:00
  • HouseUG40 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.