Time and Location

  • Speaker: Berend van Starkenburg. Leiden University Institute of Advanced Computer Science
  • Host: Prof. Lawrence S. Moss. Mathematics, Indiana University
  • Date: Wednesday, May 8
  • Time: 4:00 PM-5:15 PM
  • Location: Ballantine Hall 010

Abstract

To enable compositional reasoning for processes with shared memory, one has to understand how the properties of the behaviour of single processes can be composed into properties of the system that result from letting the processes interact via the shared memory. One option for handling this composition is so-called separation logic, which allows reasoning about memory regions and, thereby, about local views of single processes. This talk investigates compositional reasoning for interacting processes with shared memory. It proposes leveraging sheaves to amalgamate local views of processes into a cohesive specification of the global process, offering a more abstract approach to reasoning. Through a category-theoretic framework, it provides semantics for process interaction via shared memory and establishes connections between sheaves and the semantics of the standard pointer model of separation logic. The talk concludes with an outline of my ongoing research, aiming to refine local reasoning about programs within this framework and extend its applicability to extensions of separation logic.