About Me

I'm a Computer Science PhD candidate at Iowa State University in the Laboratory for Temporal Logic, advised by Kristin Yvonne Rozier. My work builds tools for delivering trust in high-assurance hardware and software systems: from design-time verification that catches bugs early to runtime monitoring that flags dangerous behavior during deployment. I hold an M.S. in Computer Science and a B.S. in Computer Engineering and Philosophy, both from Iowa State, and expect to complete my PhD in May 2027.

• PhD Candidate, Computer Science, Iowa State University (expected May 2027)
• M.S., Computer Science, Iowa State University (2024)
• B.S., Computer Engineering and Philosophy, Iowa State University (2021)
• Internships: Siemens EDA, SRI International, and Fondazione Bruno Kessler (FBK)

Research Interests

My research focuses on formal methods for high-assurance systems, spanning model checking and runtime verification of real-time, resource-constrained hardware and software platforms. I develop tools that make writing and debugging specifications easier, and algorithms that scale verification to large or infinite-state systems. These include a specification compiler used by NASA and Collins Aerospace, an intermediate language for symbolic model checking, and high-throughput monitors for temporal logic formulas. Looking ahead, I'm interested in adapting these techniques to security and privacy policies, hardware verification, and to verification artifacts, especially for Aerospace system certification (e.g., DO-333).

• C2PO / R2U2: specification compilation and runtime verification for aerospace systems
• SABRe: scalable bit-vector monitoring of Mission-time LTL
• MoXI: intermediate language and toolchain for symbolic model checking
• Infinite-state liveness checking (rlive) with FBK
• SLEC: Hardware verification at Siemens EDA (equivalence checking, abstract interpretation)

Teaching Interests

With a background spanning Computer Engineering and Computer Science, I'm interested in teaching a wide range of courses across the hardware-software spectrum, from introductory programming and discrete math to computer architecture and formal verification. I'm also interested in developing courses that survey formal techniques and hardware verification approaches through practical projects. I have lectured for two courses across six total semesters, one an introductory programming course for non-CS majors (AERE 361) and another a graduate-level formal methods course (AERE/COMS 407/507).

• Guest lecturer, Computational Techniques for Aerospace Design, AERE 361
• C structs and matrices, 3-lecture series, 3 semesters
• Guest lecturer, Applied Formal Methods, AERE/COMS 407/507
• Temporal logic, 2-lecture series, 3 semesters
• Recorded Lectures: Lecture 1 (LTL), Lecture 2 (LTL continued, CTL)
• Teaching assistant and grader for Applied Formal Methods and AERE 361
• Mentored an undergraduate on MoXI (CAV 2024); tutorials for the OpenUAS research team
• Outreach: summer STEM programs and math tutoring (grades 3–8)