Separation Logic

views comments

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

Tags

the university of edinburgh

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.

Any views expressed within media held on this service are those of the contributors, should not be taken as approved or endorsed by the University, and do not necessarily reflect the views of the University in respect of any particular issue.

Separation Logic

Related Media

the university of edinburgh