Modularity and Resource Separation

Lead Research Organisation: Queen Mary, University of London
Department Name: Computer Science


Modularity is a key concept which programmers wield in their struggle againstthe complexity of software systems. When a program is divided into conceptually distinct modules or components, each of which uses separate internal resources (such as storage),the effort required for understanding the program is decomposed into circumscribed, hopefully manageable, parts. The purpose of this project is to bring separation logic to bear on modularity.The separating conjunction connective will be used to give a precise, theoretical expression that correspondsto the existing pre-formal, intuitive link between resource separation and modularity.We will develop semantic models that describe when a piece of state used by a module is held separate from the clients that use it. Theories of refinement and parametricity will be studied. The former will begin to address one of the common criticisms of separation logic,that verifications take place on a fixed (low) level of abstraction. The latter will give us methods for showing equivalence of imperative modules and for understanding information hiding for imperative resources. We will also investigate methods for proof and static checking and analysis for imperative modules. This project contribute considerably to the problems of scalable reasoning about programs and protection of resources from outside tampering, in the presence of practical programming features such as pointers thathave previously been seen as barriers to technically precise accounts of modularity.


10 25 50
publication icon
Filipovic I (2009) Blaming the client: on data refinement in the presence of pointers in Formal Aspects of Computing

publication icon
Filipovic I (2010) Abstraction for concurrent objects in Theoretical Computer Science

publication icon
Hoare T (2008) Separation Logic Semantics for Communicating Processes in Electronic Notes in Theoretical Computer Science

publication icon
O'Hearn P (2009) Separation and information hiding in ACM Transactions on Programming Languages and Systems