Tracking Heaps that Hop with Heap-Hop

Jules Villard, Queen Mary University of London, UK

(Joint work with Etienne Lozes and Cristiano Calcagno)

Heap-Hop is a program prover for concurrent heap-manipulating programs that use message-passing synchronization. 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 of Heap-Hop to prove memory safety, race freedom, absence of memory leaks and communication safety.