| dc.description.abstract | Visualizing a model checker’s run on a model can be useful when trying to gain a deeper
understanding of the verification of the particular model. However, it can be difficult to
formalize the problem that visualization solves as it varies from person to person. Having
a visualized form of a model checker’s run allows a user to pinpoint sections of the run
without having to look through the entire log multiple times or having to know what to look
for. This thesis presents the Hubble Spacer Telescope (HST), a visualizer for Spacer, an
SMT horn clause based solver. HST combines multiple exploration graph views along with
customizable lemma transformations. HST offers a variety of ways to transform lemmas
so that a user can pick and choose how they want lemmas to be presented. HST’s lemma
transformations allow a user to change variable names, rearrange terms in a literal, and
rearrange the placement of literals within the lemma through programming by example.
HST allows users to not only visually depict a Spacer exploration log but it allows users
to transform lemmas produced, in a way that the user hopes, will make understanding a
Spacer model checking run, easier.
Given a Spacer exploration log, HST creates a raw exploration graph where clicking
on a node produces the state of the model as well as the lemmas learned from said state.
In addition, there is a second graph view which summarizes the exploration into its proof
obligations. HST uses programming by example to simplify lemma transformations so that
users only have to modify a few lemmas to transform all lemmas in an exploration log.
Users can also choose between multiple transformations to better suit their needs.
This thesis presents an evaluation of HST through a case study. The case study is used
to demonstrate the extent of the grammar created for lemma transformations. Users have
the opportunity to transform disjunctions of literals produced by Spacer into a conditional
statement, customized by the contents of the predicate. Since lemma transformations are
completely customizable, HST can be viewed as per each individual user’s preferences. | en |
