Name
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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-12002-2_23 | TACAS |
Keywords | Field | DocType |
copyless list transfer,program prover,concurrent program,hoare monitor,concurrent heap-manipulating program,memory leak,loop invariants,message-passing synchronization,parallel tree disposal,case study | Synchronization,Separation logic,Programming language,Computer science,Service provider,Heap (data structure),Loop invariant,Symbolic execution,Memory leak,Gas meter prover | Conference |
Volume | ISSN | ISBN |
6015 | 0302-9743 | 3-642-12001-6 |
Citations | PageRank | References |
12 | 0.60 | 6 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jules Villard | 1 | 66 | 4.62 |
| Étienne Lozes | 2 | 121 | 14.32 |
| Cristiano Calcagno | 3 | 12 | 0.60 |