Tracking Heaps That Hop with Heap-Hop

Abstract. Heap-Hop is a program 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 deadlock-freedom. It has been used in several case studies, including concurrent programs for copyless list transfer, service provider protocols, and load-balancing parallel tree disposal.

• Type: Conference
• Year: 2010
• Where: TACAS
• Authors: Jules Villard, Étienne Lozes, Cristiano Calcagno
• Keywords: Algorithms, Concurrent Heap-manipulating Programs, Load-balancing Parallel Tree, TACAS 2010, Types Called Contracts