Efficiently storing and matching visited states is key to the effectiveness of explicit-state model checkers such as SPIN. Models of concurrent programs often have too many reachable states to enumerate easily in main memory, and an efficient model checker can exhaust main memory in minutes by storing state descriptors exactly. A popular alternative is to over-approximate the set of visited states using a randomized, probabilistic data structure, such as a Bloom filter. Because the approximation is sound and does not slow down the search with revisitation of states, it tends to find errors quickly. Because it is probabilistically complete, the approach can also convincingly demonstrate lack of errors.
In this dissertation, I analyze the approximate state storage problem in unprecedented detail, improve upon standard solutions, and demonstrate a novel approach that solves a configuration dilemma facing users of the standard solutions. Especially with my improvements, the best Bloom filter or hash compaction configuration for a given situation is quite good, but choosing the best configuration depends on a good estimate of the number of reachable states. Such an estimate is usually only available after checking a model. I solve this dilemma with an efficient storage scheme that is not tied to a particular estimate, because it is adaptive. Regardless of the number of states encountered at run time, its accuracy is near the information-theoretic optimal. It is also competitively fast, thanks to a novel in-place adaptation algorithm and a favorable access pattern to memory.
|Commitee:||Aslam, Javed A., Cooperman, Gene, Visser, Willem|
|School Location:||United States -- Massachusetts|
|Source:||DAI-B 72/03, Dissertation Abstracts International|
|Keywords:||Bloom filter, Hash table, Hashing, Model checking, Standard solutions, Storage problem|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be