Reliable Hashing without Collosion Detection
Reliable Hashing without Collosion Detection
复制标题
可靠的散列，无需冲突检测
DOI：
10.1007/3-540-56922-7_6
复制
发表时间：
1993
期刊：
影响因子：
0.6
通讯作者：
Denis Leroy
中科院分区：
文献类型：
--
作者：
P. Wolper;Denis Leroy
由于各种新技术的出现，状态空间探索正成为验证并发程序的一种越来越有效的方法。这些技术之一，没有冲突检测的哈希，是由Holzmann提出的，作为一种大大减少存储所探索的状态空间所需的内存量的方法。不幸的是，这种内存使用的减少是以忽略部分状态空间的高概率为代价的，因此错过了现有的错误。在本文中，我们仔细分析了这种方法，并表明，通过使用修改后的策略，它是可能的，以减少错误的风险可以忽略不计的量，同时保持内存使用优势的霍尔茨曼的技术。我们提出的策略已经实施，我们描述的实验证实了良好的预期结果。
Thanks to a variety of new techniques, state-space exploration is becoming an increasingly effective method for the verification of concurrent programs. One of these techniques, hashing without collision detection, was proposed by Holzmann as a way to vastly reduce the amount of memory needed to store the explored state space. Unfortunately, this reduction in memory use comes at the price of a high probability of ignoring part of the state space and hence of missing existing errors. In this paper, we carefully analyze this method and show that, by using a modified strategy, it is possible to reduce the risk of error to a negligible amount while maintaining the memory use advantage of Holzmann's technique. Our proposed strategy has been implemented and we describe experiments that confirm the excellent expected results.