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 ,
    Towards Auditable Properties of Machine Learning Systems
    (University of Waterloo, 2026-08-24) Chantasantitam, Prach
    Machine learning (ML) property attestations are a set of mechanisms through which model providers (provers) can attest to properties about their machine learning models and datasets to verifiers, providing auditability and demonstrating compliance with regulatory or internal policies or standards. However, existing approaches do not simultaneously achieve efficiency, scalability, versatility, and security. Systems based on trusted execution environments (TEEs) have been shown to be more efficient and scalable; however, prior work is limited to CPU-only computation, making it inefficient to run large generative models. Additionally, TEE-based approaches rely on static attestation, which cannot detect run-time attacks such as loading a malicious model checkpoint or corrupting model weights in memory after the system has been launched and measured, allowing an adversary to manipulate inference outputs at run-time. As such, the limitations of existing TEE-based approaches include: (1) they do not scale to large generative models and datasets, and (2) their sole reliance on static attestation makes them vulnerable to various run-time attacks. To address the first limitation, I present PAL*M, a property attestation framework for large generative models, illustrated by large language models. PAL*M addresses three key challenges: (1) attesting properties over large datasets accessed via random sampling outside trusted memory, (2) supporting heterogeneous CPU-GPU execution environments, and (3) defining attestable properties for generative model operations. PAL*M leverages confidential virtual machines with security-aware GPUs and employs incremental multiset hashing to efficiently measure dataset integrity across memory-mapped accesses. PAL*M is implemented atop Intel TDX and NVIDIA H100, and formally modeled using the Tamarin Prover symbolic verification tool, confirming that its security guarantees are upheld under the defined threat model. For the second limitation, I present EVOLVE, a proof-of-execution (PoX) mechanism for confidential virtual machines that enables run-time property attestation of ML operations. EVOLVE has two components: an instrumentation module and a PoX monitor. The instrumentation module preprocesses an ML application to ensure that both memory accesses and indirect calls pass through the PoX monitor. At run-time, the PoX monitor inspects memory accesses to determine whether the correct subset of the application is modifying the output and validates indirect calls to ensure that control flow cannot be redirected into the monitor to alter its state, constructing PoX evidence accordingly. The PoX monitor is implemented as an extension of TD-Shim, and its efficiency and security are evaluated on Intel TDX using classifier model routing as a proof-of-concept application.
  • Thumbnail Image
    Item type: Item ,
    Investigation of a Robotic-Assisted Monocular Optical Tracking System for Navigated Spine Surgery using Modular Patient Reference Trackers
    (University of Waterloo, 2026-08-24) Hynes, Sarah
    On average, 15–18% of spinal implants are malpositioned or breach the cortical bone, leading to complications, revision surgeries, and increased healthcare costs. To improve surgical accuracy and patient outcomes, image-guided navigation systems have been developed to localize surgical instruments and critical anatomy while assisting with implant placement. By providing real-time visualization relative to pre-operative medical images, these systems reduce the need for repeated intra-operative imaging, improving accuracy while decreasing radiation exposure and the likelihood of revision procedures. Despite these advantages, current optical navigation systems remain susceptible to line-of-sight interruptions, which can result in tracking loss and disrupt the surgical workflow. To address these limitations, the objectives of this research were to: (1) compare the tracking performance of stereo and monocular optical tracking systems for spinal navigation, (2) develop and validate a modular patient reference tracker mounting system capable of supporting automatic registration using overhead tracking, and (3) integrate the proposed registration workflow into an augmented reality navigation framework. The first objective was achieved through a comparative evaluation of stereo and monocular tracking systems while tracking an identical rigid body. Both systems demonstrated tracking accuracy within clinically acceptable limits, indicating that the smaller-footprint monocular camera represents a viable alternative to conventional stereo tracking systems. Given the high level of agreement observed between the two cameras, selection may instead be based on operating room constraints and surgeon workflow requirements rather than tracking performance alone. The second objective demonstrated that the modular mounting system provided repeatable positioning of the patient reference tracker with minimal localization error across mounting positions. Although tracking accuracy degraded slightly as the camera offset increased, the observed errors remained within clinically acceptable limits. Furthermore, the mounting system maintained consistent registration when a single point-to-point registration was used across multiple patient reference tracker positions, demonstrating that repositioning did not necessitate repeated manual registration. While the proposed CT-based automatic registration workflow did not achieve clinically acceptable target registration error, it demonstrated sub-millimeter localization accuracy of the patient reference tracker and identified the primary sources of error, suggesting that the methodology could be further improved through secondary registration refinement and improvements to the experimental hardware. The final objective resulted in the development of an open-source augmented reality framework within 3D Slicer that integrates camera calibration, optical tracking, and CT-based registration for real-time anatomical visualization. Using user-defined camera intrinsics, the framework establishes the spatial relationship between the surgical exoscope and the optical tracking system, enabling tracked surgical instruments, patient reference trackers, and pre-operative anatomical information to be projected directly onto the exoscope image. By leveraging the proposed automatic registration workflow, anatomical landmarks identified on the pre-operative CT can be visualized within the surgical field, providing intuitive guidance for tasks such as incision planning, anatomical localization, and spinal implant positioning.
  • Thumbnail Image
    Item type: Item ,
    Adolescent Mentalizing Across Online and Offline Contexts: The Role of Perspective, Temperament, and Online Communication
    (University of Waterloo, 2026-08-24) Aravinthan, Kowsi
    Successfully navigating the complex social demands of adolescence requires the ability to accurately infer and interpret others' mental states. However, relatively little is known about the contextual and individual factors that shape adolescent mentalizing. With peer interactions increasingly taking place online, the present study examined whether adolescents mentalize differently across online and offline communication contexts, whether these differences depend on the perspective adopted (self- vs. other-referential), and whether temperamental shyness and frequency of online communication are associated with adolescent mentalizing. Two samples of younger (13–16 years; N = 80) and older (17–19 years; N = 264) adolescents completed the Mentalizing Across Contexts Task, a novel vignette-based measure assessing mentalizing bias across online and offline peer interactions. Participants rated the likelihood of negative, neutral, and positive mental state interpretations from both self-referential (inferring how a peer would think about them) and other-referential (inferring their own thoughts about a peer) perspectives. Participants also completed measures of temperamental shyness and online communication engagement. Across both samples, adolescents’ mental state inferences varied by communicative context and perspective. Greater negative mentalizing was endorsed in offline compared with online interactions and when adolescents inferred how peers might think about them rather than their own thoughts about another peer. Higher levels of temperamental shyness were associated with greater negative mentalizing, particularly during self-referential mentalizing, whereas more frequent online communication was associated with greater negative mentalizing across both communicative context and perspective. Implications for theory, future research, and intervention are discussed.
  • Thumbnail Image
    Item type: Item ,
    Reducing CTL-live model checking to semantic entailment in first-order logic (version 1)
    (University of Waterloo, 2014-03-20) Vakili, Amirhossein; Day, Nancy A.
    The core of temporal logic model checking is the reachability problem, which is not expressible in first-order logic (FOL). Most model checking algorithms, both for finite and infinite Kripke structures, contain a loop that iterates to reach a fixed-point. As a result, reasoners with input languages no more expressive than FOL have been used iteratively for model checking rather than having the reasoner solve the problem completely by itself. In this article, we present a method for reducing model checking of finite and infinite Kripke structures that are expressed in FOL to entailment checking in FOL for a fragment of computational tree logic (CTL), which we call CTL-live. CTL-live includes all the CTL connectives that are expressible in the mu-calculus using the least fixed-point operator. These connectives are traditionally used to express liveness properties. This reduction allows us to consider model checking of CTL-live as a FOL theorem proving problem, and to use directly FOL reasoning techniques for model checking without the need of fixed-point operators, transitive-closure, or induction. We prove that CTL-live is maximal in the sense that model checking of CTL connectives that are not included in CTL-live is not reducible to semantic entailment in FOL.
  • Thumbnail Image
    Item type: Item ,
    A multiagent-based simulation model to support management decision making in software development
    (University of Waterloo, 2014-03-06) Baina, Davy; Lucena, Carlos J. P.; Cowan, Donald; Bommel, Pierre; Valdares, Carolina; Oliveira, Toacy
    Context Techniques to support the development of software projects and describe the quality of the results have received substantial attention from the research community because software projects often do not achieve their intended results in terms of factors such as time to completion and quality of the final product. Objective In this paper, we propose a MultiAgent-Based Simulation Model to support project managers in the decision-making process that is required in the creation of software systems. This model is based on the Project Management Body of Knowledge (PMBOK) in areas such as cost, time, scope and human resources. Methods We present an illustrative example that was drawn from our experience with real-world software development projects conducted within our research group. Such an example demonstrates the benefits and drawbacks of using MultiAgent System simulation as a support tool for the project manager's decision-making process. Results We have created a simulation model and associated scenarios that allow a project manager to analyze strategic options throughout the project. Each option is based on the PMBOK practices allowing project managers to investigate the best scenario that meets the project needs such as cost, time and quality. Conclusions Some factors are crucial to the success or failure of a project. Decisions made by the project manager are one such set of factors that determine if the project goals are achievable. Through using MABS to simulate scenarios we have become convinced that this approach can contribute to the understanding of the phenomena that occur during a software development project and provide real assistance to the project manager.