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.