FMCAD 2004 START ConferenceManager    


Bloom Filters in Probabilistic Verification

Peter C. Dillinger and Panagiotis Manolios

Presented at Formal Methods in Computer-Aided Design (FMCAD 2004), Austin, Texas, November 14-17, 2004


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 criticised 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 compuational 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 validate our work and analyses with extensive testing using 3SPIN, a model checker we developed by extending SPIN.


  
START Conference Manager (V2.46.3)
Maintainer: sanders@cs.ubc.ca