Heap-Hop is a prover for concurrent heap-manipulating programs that use Hoare monitors and 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. Heap-Hop can prove safety and race-freedom and, thanks to contracts, absence of memory leaks and safety of communications.

You can find out more about Heap-Hop in the papers section.



The people involved are: