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.
- June-July 2011: Ioana Cristescu (ENS Lyon) came for a two month internship at Queen Mary University for her Master to work on improving Heap-Hop's theory and implementation. She added support for message parameters, which let you track message values accross time in the logic, and for arrays.
- 23 Mar. 2010: Heap-Hop is presented to the public at TACAS in Cyprus.
- 9 Feb. 2010: A repository of Heap-Hop is up on bitbucket.
- 11 Dec. 2009: Our tool paper has been accepted at TACAS'10.
- 12 Oct. 2009: Heap-Hop version 1.0 is out. Check it out!
The people involved are: