Séminaires des équipes de recherche
Separation Logic for Non-local Control Flow and Block Scope Variables
- 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.