Advances in Programming Languages 2018/19 Lecture 14: Separation Logic
Hoare Logic is a language for making and proving assertions about the behaviour of code: the extension to Separation Logic introduces ways to describe how programs use complex memory structures. Statements in separation logic specify the behaviour of memory cells, the heap, pointers and pointer arithmetic, as well as allocation and deallocation of storage. These can be combined to prove properties of datastructures like linked lists, trees, and queues and also the algorithms that operate on them.
This lecture introduced the basic operations of separation logic, outlined how they can be applied, and discussed some of their impact on industrial practice.
Media Hopper Create does not permit public attachments to videos, so for the corresponding slides you will need to use this alternate server:
https://wp.inf.ed.ac.uk/apl18/wp-content/uploads/sites/10/2018/11/apl18-14.pdf