salle A. Turing CE4
10 December 2014 - 14h00
An Introduction to Separation Logic
by Cristina Serban from VERIMAG
Abstract: Separation logic is a novel system for reasoning about program correctness, which extends Hoare logic by allowing reasoning over the state of the heap. It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang and is based on early work by Rod Burstall. Separation logic facilitates reasoning about shared mutable data structures and also supports local reasoning. It has also been extended to deal with other situations, such as shared-variable concurrency or information hiding. The purpose of this seminar is to offer an introduction to separation logic and serve as training for the lectures that will be given by Prof. Chin Wei Ngan in Verimag on December 12, 16 and 18.
