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.
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336, VAT Registration Number GB 592 9507 00, and is acknowledged by the UK authorities as a “Recognised body” which has been granted degree awarding powers.