UWSpace will be migrating to a new version of its software from July 29th to August 1st. UWSpace will be offline for all UW community members during this time.

Show simple item record

dc.contributor.authorRamanathan, Aishwarya
dc.date.accessioned2022-01-19 16:31:32 (GMT)
dc.date.available2022-01-19 16:31:32 (GMT)
dc.description.abstractVisualizing 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
dc.publisherUniversity of Waterlooen
dc.subjectmodel checkingen
dc.subjectprogramming by exampleen
dc.titleHubble Spacer Telescopeen
dc.typeMaster Thesisen
uws-etd.degree.departmentDavid R. Cheriton School of Computer Scienceen
uws-etd.degree.disciplineComputer Scienceen
uws-etd.degree.grantorUniversity of Waterlooen
uws-etd.degreeMaster of Mathematicsen
uws.contributor.advisorTrefler, Richard
uws.contributor.advisorGurfinkel, Arie
uws.contributor.affiliation1Faculty of Mathematicsen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages