Browsing Theses by Supervisor "Gurfinkel, Arie"
Now showing items 1-6 of 6
-
Bounded Model Checking of Industrial Code
(University of Waterloo, 2021-09-14)Abstract: Bounded Model Checking(BMC) is an effective and precise static analysis technique that reduces program verification to satisfiability (SAT) solving. However, with a few exceptions, BMC is not actively used in ... -
Decompilation of Binaries into LLVM IR for Automated Analysis
(University of Waterloo, 2022-01-25)Complexity in malicious software is increasing to avoid detection and mitigation. As such, there is greater interest in using automation for reverse engineering. Current state-of-the-art tools use proprietary intermediate ... -
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 ... -
Strong Induction in Hardware Model Checking
(University of Waterloo, 2019-08-14)Symbolic Model checking is a widely used technique for automated verification of both hardware and software systems. Unbounded SAT-based Symbolic Model Checking (SMC) algorithms are very popular in hardware verification. ...