Bloom Filters in Probabilistic Verification

12 years 7 months ago
Bloom Filters in Probabilistic Verification
Abstract. Probabilistic techniques for verification of finite-state transition systems offer huge memory savings over deterministic techniques. The two leading probabilistic schemes are hash compaction and the bitstate method, which stores states in a Bloom filter. Bloom filters have been criticized for being slow, inaccurate, and memory-inefficient, but in this paper, we show how to obtain Bloom filters that are simultaneously fast, accurate, memory-efficient, scalable, and flexible. The idea is that we can introduce large dependences among the hash functions of a Bloom filter with almost no observable effect on accuracy, and because computation of independent hash functions was the dominant computational cost of accurate Bloom filters and model checkers based on them, our savings are tremendous. We present a mathematical analysis of Bloom filters in verification in unprecedented detail, which enables us to give a fresh comparison between hash compaction and Bloom filters. Finally, we...
Peter C. Dillinger, Panagiotis Manolios
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Authors Peter C. Dillinger, Panagiotis Manolios
Comments (0)