Loading...

James Brotherston - An Introduction to Separation Logic

1,286 views

Loading...

Loading...

Loading...

Rating is available when the video has been rented.
This feature is not available right now. Please try again later.
Published on Jan 18, 2016

Dr James Brotherston presents his talk on "An Introduction to Separation Logic" at Oracle Labs in Brisbane Australia.

James Brotherston
University College London

In this talk, I introduce separation logic, a popular formalism for verifying pointer programs that is now seeing use in industrial-strength verification tools such as Facebook's Infer (fbinfer.com). Like other program logics, separation logic is built from three main components: (1) a programming language; (2) a language of logical assertions for talking about program states; and (3) a language of program judgements (here, Hoare triples) for relating programs to assertions. The characteristic feature of separation logic is its use of the separating conjunction (*) in its assertion language to denote disjoint portions of heap memory. Since the commands of our language act only locally on memory, a version of the well-known frame rule holds in separation logic, which enables us to construct proofs of whole programs compositionally from proofs of its component procedures.

James Brotherston - http://www0.cs.ucl.ac.uk/people/J.Bro...

Oracle Labs Australia - https://labs.oracle.com/locations/aus...

Loading...

When autoplay is enabled, a suggested video will automatically play next.

Up next


to add this to Watch Later

Add to

Loading playlists...