Separation Logic

From Ian Stark on March 2nd, 2019

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.

Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh 2019. Course specific materials are created by University of Edinburgh staff for you to use in your studies. You should not share, publish or sell these outside the University

Separation Logic

Related Media

the university of edinburgh