Sites Inria

Version française

Séminaires des équipes de recherche

Separation Logic for Non-local Control Flow and Block Scope Variables

Séminaire Gallium - Moscova

  • Date : 4/02/2013
  • Place : Inria - Rocquencourt - Amphithéâtre Alan Turing
  • Guest(s) : Robert Krebbers - Radboud University Nijmegen
  • Organiser(s) : Gallium - Moscova

We present an approach for handling non-local control flow (goto and return statements) in the presence of allocation and deallocation of block scope variables in imperative programming languages.
We define a small step operational semantics and an axiomatic semantics (in the form of a separation logic) for a small C-like language that combines these two features, and which also supports pointers to block scope variables. Our operational semantics represents the program state through a generalization of Huet's zipper data structure.
We prove soundness of our axiomatic semantics with respect to our operational semantics. This proof has been fully formalized in Coq.

Keywords: Paris - Rocquencourt Séminaire Moscova Gallium