University of Cambridge > > Semantics Lunch (Computer Laboratory) > Locality and Footprints in Separation Logic

Locality and Footprints in Separation Logic

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

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.

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