(Stellenbosch : Stellenbosch University, 2018-03) Breytenbach, Jean Anré; Fischer, Bernd; Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences (Computer Science)

Show more

ENGLISH ABSTRACT : Program verification is a computationally expensive and time-consuming process.
Bounded model checking is a branch of program verification that produces FOL formulas
to be checked for satisfiability by an SMT solver. These formulas encode state
transitions to states where property violations will occur and the SMT solver attempts
to find a list of variable assignments that would create a path to one of these states.
Bounded model checking tools create these formulas by iteratively increasing an unwind
bound k that dictates the number of transitions that can be present in a path, for
each unwind bound k all possible paths of length k are generated. Any state containing
a property violation that is generated during the unwind bound k − 1 should also be
present during the unwind bound k with perhaps a longer path to reach it.
This creates many of the same paths being checked during each subsequent iteration
causing the SMT solver to potentially perform duplicate work. This thesis seeks to
build and evaluate a formula cache in which to store parts of the formula for which the
satisfiability is already known. During subsequent iterations the formula can be sliced
by removing the parts that are found in the cache, providing smaller formulas for the
SMT solver which should take less time to solve. Similar formula caches have already
proven successful in the field of symbolic execution.
Multiple techniques are described to modify the formulas to increase the likelihood
of finding a match in the cache and these techniques are combined in a multitude of
ways to generate a collection of caching strategies. These strategies are then evaluated
against multiple data sets to find the best performing strategies and to identify the types
of problems that benefit the most from caching. The results are then compared to the
results of caching formulas during symbolic execution to gain insight as to how these
different approaches effectively implement caching.