![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
John Wickerson (University of Cambridge)
Monday 26 October 2009, 12:45-14:00
Verifying malloc using RGSep and 'Explicit Stabilisation'
- 👤 Speaker: John Wickerson (University of Cambridge)
- 📅 Date & Time: Monday 26 October 2009, 12:45 - 14:00
- 📍 Venue: Room FW26, Computer Laboratory, William Gates Building
Abstract
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.
Series This talk is part of the Semantics Lunch (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Department of Computer Science and Technology talks and seminars
- Interested Talks
- Martin's interesting talks
- Room FW26, Computer Laboratory, William Gates Building
- School of Technology
- Semantics Lunch (Computer Laboratory)
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.