Resource Reasoning and Labelled Separation Logic

Separation logic has led to many advances in modular and scalable verification of heap-manipulating programs through the spatial reasoning that it provides. This approach however does not address some of the deeper properties of program executions that are important for program optimizations (e.g. automatic parallelization) and inferring dynamic resource ownership transfers in concurrent program executions. In this talk I will describe a technique of symbolic resource labelling with separation logic and its application to the precise tracking of resource manipulation in program executions. This has been used for detecting memory access dependences between distant program statements, and has been applied in the synthesis of optimized hardware circuits from C programs. I will also describe a related labelling technique for analysing resource sharing in concurrent programs, which tracks the dynamic transfers of ownership between concurrent processes and can be used for automating concurrent separation logic proofs.