Jules Villard (Queen Mary): Tracking Heaps that Hop with Heap-Hop
Abstract: Heap-Hop is a program prover for concurrent heap-manipulating programs that use message-passing synchronization over a shared memory. Programs are annotated with pre and post-conditions and loop invariants, written in a fragment of separation logic. Communications are governed by a form of session types called contracts. Logic and contracts collaborate inside Heap-Hop to prove memory safety, race freedom, absence of memory leaks and communication safety.