I'm a Computer Science PhD candidate at Iowa State University in the Laboratory for Temporal Logic, advised by Kristin Yvonne Rozier. 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, and Fondazione Bruno Kessler (FBK)

Research Interests

I am interested in building the tools and techniques for ensuring that high-assurance systems such as spacecraft, aircraft, self-driving cars, and chip designs operate safely and efficiently. My tools include a specification compiler for real-time monitoring of embedded systems currently used by groups in NASA and Collins Aerospace. I also work on scalable model checking tools and algorithms for large-scale systems. In the near future, I am 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 am interested in teaching a wide range of courses across the computing spectrum, from introductory programming and discrete math to computer architecture, formal verification, and digital logic. 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)
• Outreach: summer STEM programs and math tutoring (grades 3–8)