Modelling storage and resources: an introduction to separation logic

Dave Schmidt - Computing and Information Sciences Department, Kansas State University, USA
Data e ora
martedì 13 luglio 2004 alle ore 17.00
Ca' Vignal - Piramide, Piano 0, Sala Verde
Roberto Giacobazzi
Referente esterno
Data pubblicazione
5 luglio 2004


Programs, processes, resources, and storage heaps are often
modelled by graphs, and correctness properties are validated on the
graphs. The correctness proofs are often complicated because the graph's
nodes are _shared_ by the graph's edges.

Separation logic, developed by O'Hearn, Reynolds, and Yang,
is a simple extension of Hoare logic for writing compositional
correctness proofs for such graphs.

In this introductory presentation, we review Hoare logic,
show the difficulties that arise when there is sharing of resources,
and show how separation logic removes (some of) the difficulties. We
apply separation logic to example programs that manipulate storage heaps
and shared resources.

© 2002 - 2021  Universit√† degli studi di Verona
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234