Locality and Footprints in Separation Logic

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

• Mohammad Raza (Imperial College)
• Monday 19 October 2009, 12:45-14:00
• Room FW26, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Sam Staton.

Local reasoning based on separation logic captures the natural local behaviour of programs by allowing reasoning to focus on the footprints of commands. In the semantic formalization of abstract separation logic, programs are modelled as “local functions” that act locally on abstract resource models. However, certain issues related to dynamic allocation force some non-intuitive choices in the general definition of locality, and lead to some unnatural outcomes. For example, the safety footprints of a program do not always yield a complete specification of the program, and one is forced to work with non-deterministic allocation in unbounded memory. We investigate these issues, and first present a formalization of “completeness footprints” which yield complete specifications. We then present an alternative memory model in which completeness footprints do correspond to safety footprints, and deterministic or bounded memory allocation can be modelled as local functions. More generally, a stronger notion of locality is identified which provides the correspondence between safety and completeness footprints for arbitrary resource models.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Room FW26, Computer Laboratory, William Gates Building
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.