University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > Verifying malloc using RGSep and 'Explicit Stabilisation'

Verifying malloc using RGSep and 'Explicit Stabilisation'

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

If you have a question about this talk, please contact Sam Staton.

The talk will introduce a new formalisation of stability for Rely-Guarantee, in which an assertion’s stability is encoded into its syntactic form. I’ll briefly show how this allows library code to be specified independently of its various calling environments. But the main thrust of the talk concerns how this so-called ‘explicit stabilisation’ can be applied to RGSep, a recent addition to the Rely-Guarantee family. Doing so enables an ‘InfoHiding’ rule, which describes how a (sequential) module can hide its ‘internal interference’ from clients. We illustrate with a proof of the memory management module from Version 7 Unix.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity