Friends
We list some projects related to Heap-Hop below.
- Smallfoot is the tool Heap-Hop is based on. Big ups to them!
- SmallfootRG extends Smallfoot with Rely-Guarantee reasoning.
- Chalice is a program prover that also supports copyless message passing. Unlike Heap-Hop however, it does not rely on contracts.
- The Singularity project and the associated language have inspired our work on copyless message passing and contracts.
Libraries
Heap-Hop uses the following libraries:
- Shares are modelled using the Mechanized Semantics Library. Their shares implementation is included in Heap-Hop source code.
- Heap-Hop uses dot to draw graphical representations of contracts.
- There is an old, outdated GUI included with Heap-Hop for which you need lablgtk.