UWSpace

UWSpace is the University of Waterloo’s institutional repository for the free, secure, and long-term home of research produced by faculty, students, and staff.

Depositing Theses/Dissertations or Research to UWSpace

Are you a Graduate Student depositing your thesis to UWSpace? See our Thesis Deposit Help and UWSpace Thesis FAQ pages to learn more.

Are you a Faculty or Staff member depositing research to UWSpace? See our Waterloo Research Deposit Help and Self-Archiving pages to learn more.

Photo by Waterloo staff

Communities in UWSpace

Select a community to browse its collections.

Recent Submissions

  • Thumbnail Image
    Item type: Item ,
    Spatial-Temporal Computer Vision Methods for Automated Vision-Based Visual Inspection
    (University of Waterloo, 2026-06-08) Midwinter, Max Xuhao Xue
    The objective of this thesis is to investigate how spatial and temporal context can be leveraged to enhance automated vision-based visual inspection (AVVI). The prevailing paradigm in AVVI is the single-shot supervised deep semantic inference model, where an image is processed independently and the resulting semantic prediction is compared against labeled data to generate a supervision signal. While these methods have demonstrated strong performance for defect detection tasks, they often neglect the spatial and temporal context in which inspection data are collected. In practice, engineers rarely make decisions based on a single observation in isolation; instead, they rely on contextual information such as multiple viewpoints of a region of interest, geometric cues for estimating defect scale, and comparisons with previous inspection records. This thesis therefore explores how contextual information inherent in inspection workflows can be incorporated directly into the inference process. Three research challenges are investigated in my thesis: leveraging multi-view imagery to improve defect segmentation, developing and evaluating spatial inference models for defect quantification in civil infrastructure, and enabling visual change detection between unordered sets of inspection data. In Chapter 3, multi-view spatial relationships between inspection images are used to refine segmentations from an unsupervised feature-clustering semantic segmentation model through a novel iterative stochastic consensus algorithm. In Chapter 4, a civil infrastructure RGB-D dataset is created using a custom handheld Light Detection and Ranging scanner, consisting of five short- to medium-span overpass bridges used to benchmark monocular metric depth estimation methods for defect measurement. In Chapter 5, synchronized pairs of novel view synthesis models are constructed to generate pixel-aligned renders of the same structure across inspection events, enabling visual change detection. Finally, Chapter 6 discusses the implications of this research for industrial inspection workflows and possible directions for future work.
  • Thumbnail Image
    Item type: Item ,
    From Mock Environments to Ownership-Aware Compilation: Practical Advances in Low-Level Program Reasoning
    (University of Waterloo, 2026-06-08) Priya, Siddharth
    Automated reasoning can improve both the correctness and the performance of systems software. In practice, however, such reasoning matters only when it fits how developers build software and when it scales to realistic codebases. In verification, one workflow challenge is that the cost of modeling the surrounding environment can exceed the cost of verifying the system itself. Another practical difficulty is scaling precise low-level reasoning and optimization to larger bodies of code. To address these problems, this work develops verification and optimization tools built over a low-level intermediate representation, LLVM-IR, integrating directly with existing compiler toolchains. The thesis first addresses developer workflow friction in verification. vMocks introduces testing-style mocks to code-level formal verification, bringing a familiar testing idiom for specifying environments to a setting where environment modeling is a significant barrier. Instead of building full environment models, developers specify unit-local behavior through SeaMock, a compile-time C++ library compatible with symbolic execution. On the Android Trusty TEE communication layer and the mbedTLS cryptographic library, this approach substantially reduces unit-proof development effort relative to full environment models. The verify-rust case study extends this workflow-oriented perspective to mixed safe–unsafe Rust programs, where the type system alone cannot enforce whole-program properties such as panic freedom and memory safety. This case study builds on SEABMC, a bit-precise bounded model checker for LLVM-IR introduced in prior work. Because SEABMC operates on LLVM-IR, it verifies these properties directly on the bitcode that the Rust compiler already produces. This lets the approach fit into existing Rust toolchains used in production without requiring a custom frontend. The thesis then addresses scale by preserving and exploiting ownership semantics in low-level reasoning and optimization. Cache-at-Pointer and SeaUrchin show that ownership information from high-level languages can remain useful after lowering to low-level representations. Cache-at-Pointer develops ownership semantics for an LLVM-like IR. It then uses a pointer cache to simplify low-level memory reasoning by modeling some memory accesses directly at the pointer rather than through a shared address space. SeaUrchin maps Rust’s ownership discipline to LLVM-IR, preserving semantic structure that is normally discarded during compilation and making it available to optimization. As a case study, ownership-aware loop-invariant code motion shows that the preserved ownership information improves LICM efficacy on realistic Rust benchmarks. Together, these two phases form a single arc: low-level automated reasoning becomes more useful when it better fits developer workflows and when it preserves enough semantic structure to scale. The thesis therefore advances formal verification and compilation not as isolated techniques, but as parts of software engineering practice.
  • Thumbnail Image
    Item type: Item ,
    Impact of a single bout of aerobic exercise on regional brain perfusion and activation responses in healthy young adults
    (Public Library of Science, 2014-01-08) MacIntosh, Bradley J.; Crane, David E.; Sage, Michael D.; Rajab, A. Saeed; Donahue, Manus J.; McIlroy, William E.; Middleton, Laura E.
    Purpose Despite the generally accepted view that aerobic exercise can have positive effects on brain health, few studies have measured brain responses to exercise over a short time span. The purpose of this study was to examine the impact within one hour of a single bout of exercise on brain perfusion and neuronal activation. Methods Health adults (n=16; age range: 20-35 yrs) were scanned using Magnetic Resonance Imaging (MRI) before and after 20 minutes of exercise at 70% of their age-predicted maximal heart rate. Pseudo-continuous arterial spin labeling (pcASL) was used to measure absolute cerebral blood flow (CBF) prior to exercise (pre) and at 10 min (post-10) and 40 min (post-40) post-exercise. Blood oxygenation level dependent (BOLD) functional MRI (fMRI) was performed pre and post-exercise to characterize activation differences related to a go/no-go reaction time task. Results Compared to pre-exercise levels, grey matter CBF was 11% (±9%) lower at post-10 (P<0.0004) and not different at post-40 (P = 0.12), while global WM CBF was increased at both time points post-exercise (P<0.0006). Regionally, the hippocampus and insula showed a decrease in perfusion in ROI-analysis at post-10 (P<0.005, FDR corrected), whereas voxel-wise analysis identified elevated perfusion in the left medial postcentral gyrus at post-40 compared to pre (pcorrected = 0.05). BOLD activations were consistent between sessions, however, the left parietal operculum showed reduced BOLD activation after exercise. Conclusion This study provides preliminary evidence of regionalized brain effects associated with a single bout of aerobic exercise. The observed acute cerebrovascular responses may provide some insight into the brain's ability to change in relation to chronic interventions.
  • Thumbnail Image
    Item type: Item ,
    An assessment of health risks and mortality from exposure to secondhand smoke in Chinese restaurants and bars
    (Public Library of Science, 2014-01-08) Liu, Ruiling; Jiang, Yuan; Li, Qiang; Hammond, S. Katharine
    Introduction Smoking is generally not regulated in restaurants or bars in China, or the restrictions are not fully implemented if there are any, while the related hazard health effects are not recognized by the majority of the Chinese population. Objectives This study aims to assess the excess health risks and mortality attributed to secondhand smoke (SHS) exposure in restaurants and bars for both servers and patrons to provide necessary evidence for advancing tobacco control in this microenvironment. Methods Two approaches were used for the assessment. One is a continuous approach based on existing field measurements and Repace and Lowrey's dose-response model, and the other is a categorical approach base don exposure or not and epidemiological studies. Results Based on the continuous approach, servers were estimated to have a lifetime excess risk (LER) of lung cancer death (LCD) of 730 to 1,831×10−6 for working five days a week for 45 years in smoking restaurants and 1,862 to 8,136×10−6 in smoking bars, and patrons could have a LER of LCD of 47 to 117×10−6 due to visiting smoking restaurants for an average of 13 minutes a day for 60 years, and 119 to 522×10−6 due to visiting smoking bars. The categorical approach estimated that SHS exposure in restaurants and bars alone caused 84 LCD and 57 ischemic heart disease (IHD) deaths among nonsmoking servers and 1,2419 LCDs and 1,689 IHD deaths among the nonsmoking patron population. Conclusions SHS exposure in restaurants and bars alone can impose high lifetime excess risks of lung cancer death and ischemic heart disease deaths to both servers and patrons, and can cause a significant number of deaths each year in China. These health risks and deaths can be prevented by banning smoking in restaurants and bars and effectively implementing these smoking bans.
  • Thumbnail Image
    Item type: Item ,
    A large-scale allosteric transition in cytochrome P450 3A4 revealed by luminescence resonance energy transfer (LRET)
    (Public Library of Science, 2013-12-23) Sineva, Elena V.; Rumfeldt, Jessica A. O.; Halpert, James R.; Davydov, Dmitri R.
    Effector-induced allosteric transitions in cytochrome P450 3A4 (CYP3A4) were investigated by luminescence resonance energy transfer (LRET) between two SH-reactive probes attached to various pairs of distantly located cysteine residues, namely the double-cysteine mutants CYP3A4(C64/C468), CYP3A4(C377/C468) and CYP3A4(C64/C121). Successive equimolar labeling of these proteins with the phosphorescent probe erythrosine iodoacetamide (donor) and the near-infrared fluorophore DY-731 maleimide (acceptor) allowed us to establish donor/acceptor pairs sensitive to conformational motions. The interactions of all three double-labeled mutants with the allosteric activators α-naphthoflavone and testosterone resulted in an increase in the distance between the probes. A similar effect was elicited by cholesterol. These changes in distance vary from 1.3 to 8.5 Å, depending on the position of the donor/acceptor pair and the nature of the effector. In contrast, the changes in the interprobe distance caused by such substrates as bromocriptine or 1-pyrenebutanol were only marginal. Our results provide a decisive support to the paradigm of allosteric modulation of CYP3A4 and indicate that the conformational transition caused by allosteric effectors increases the spatial separation between the beta-domain of the enzyme (bearing residues Cys64 and Cys377) and the alpha-domain, where Cys121 and Cys468 are located.