Verifying malloc using RGSep and 'Explicit Stabilisation'

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

• John Wickerson (University of Cambridge)
• Monday 26 October 2009, 12:45-14:00
• Room FW26, Computer Laboratory, William Gates Building.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Computer Laboratory talks
• Room FW26, Computer Laboratory, William Gates Building
• School of Technology
• Semantics Lunch (Computer Laboratory)
• de239's list

Note that ex-directory lists are not shown.