Tracking Heaps That Hop with Heap-Hop

Tracking Heaps That Hop with Heap-Hop
复制标题

使用 Heap-Hop 跟踪跳跃的堆

DOI：
10.1007/978-3-642-12002-2_23
复制
发表时间：
2010
期刊：
Proceedings of the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering
影响因子：
--
通讯作者：
Cristiano Calcagno
Cristiano Calcagno
中科院分区：
--
文献类型：
--
作者：
Jules Villard;É. Lozes;Cristiano Calcagno

文献摘要

被引文献

相似文献

Heap-Hop是用于使用HOARE监视器和通过消息同步的并发堆操作程序的程序权度。程序带有前提条件和后的和循环不变的注释，并以分离逻辑的片段编写。通信由一种称为合同的会话类型的形式管辖。堆霍普可以证明安全性和种族自由，并且由于合同，没有记忆泄漏和死锁自由。它已在几个案例研究中使用，包括用于无拷贝列表转移，服务提供商协议和负载平衡并行树处置的同时程序。
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.