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

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

• Bernhard Reus, University of Sussex
• Friday 03 November 2006, 14:00-15:00
• FW11.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory talks
• Computing and Mathematics
• FW11
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.