Browsing Theses by Supervisor "Trefler, Richard"
Now showing items 1-5 of 5
-
Hubble Spacer Telescope
(University of Waterloo, 2022-01-19)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 ... -
Local Reasoning for Parameterized First Order Protocols
(University of Waterloo, 2019-08-14)First Order Logic (FOL) is a powerful reasoning tool for program verification. Recent work on Ivy shows that FOL is well suited for verification of parameterized distributed systems. However, specifying many natural objects, ... -
Smart Contract Analysis Through Communication Abstractions
(University of Waterloo, 2021-09-07)Smart contracts are programs that manage interactions between many users. Recently, Solidity smart contract have become a popular way to enforce financial agreements between untrusting users. However, such agreements do ... -
Symmetry Reduction and Compositional Verification on Timed Automata
(University of Waterloo, 2017-08-24)This thesis is about techniques for the analysis of concurrent and real-time systems. As the first contribution, we describe a technique that incorporates automatic symmetry detection and symmetry reduction in the ... -
Verifying Mutable Systems
(University of Waterloo, 2017-10-23)Model checking has had much success in the verification of single-process and multi-process programs. However, model checkers assume an immutable topology which limits the verification in several areas. Consider the security ...