[Colloq] PhD Thesis Defense - Peter Dillinger, Tuesday, Dec. 14

[Rachel Kalweit]

The College of Computer and Information Science presents:

Thesis Defense by:
Peter Dillinger

Date: December 14, 2010 (Tues.) 
Time: 8:00 AM
(time chosen to accommodate committee members in other time zones)
Where: West Village H, Room 366

Thesis title: Adaptive Approximate State Storage

Abstract:

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.

Thesis committee:

Javed Aslam
Gene Cooperman
Pete Manolios (thesis advisor)
Willem Visser (University of Stellenbosch, external member)