University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Reasoning about Code Pointers (Separation Logic for Higher-Order Store)

Reasoning about Code Pointers (Separation Logic for Higher-Order Store)

Add to your list(s) Download to your calendar using vCal

  • UserBernhard Reus, University of Sussex
  • ClockFriday 03 November 2006, 14:00-15:00
  • HouseFW11.

If you have a question about this talk, please contact Tom Ridge.

Separation Logic is a sub-structural logic that supports local reasoning for imperative programs with heaps. It is designed to elegantly describe sharing and aliasing properties of heap structures, thus facilitating the verification of programs with pointers. So far, various flavours of separation logic have been developed for heaps containing records of basic data types. Yet, languages like C or ML also allow procedures to be stored on the heap. Such type of heap is commonly referred to as “higher-order store’’. > This talk addresses the problem of lifting Separation Logic from first-order to higher-order store. To that end we endow a simple language including dynamic memory management with a Hoare-style logic featuring Separation Logic connectives. To prove soundness, Denotational Semantics is employed throughout but not just for conceptual clarity. Modeling higher-order store as recursive domain enables us to use powerful (and well established) results from Domain Theory. This approach also admits an elegant re-use of a proof rule we introduced in previous work to deal with recursion through the store.

This is joint work with Jan Schwinghammer, Programming Systems Lab, Saarland University.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity