My Work
Publications
| Title | Venue |
|---|---|
| The Proof Must Go On: Formal Methods in the Theater of Secure Software Development of
the Future
Draft Reviews Revised Draft Revision Cover Letter Publication Presentation Presentation Recording |
SPLASH Onward! Essays 2025 |
| Formally-Verified, Tight Timing Constraints for Machine Code
Gold Award Winner Draft Reviews Extended Abstract Poster Finals Presentation Finals Presentation Recording |
PLDI SRC 2025 |
| VOLPIC: Verifying Lifted Pascal in Coq
Draft Reviews Extended Abstract Poster |
PLDI SRC 2024 |
| Prettybird: A DSL for Programmatic Font Compilation
Draft Reviews Extended Abstract Poster |
PLDI SRC 2023 |
| Self-Supervised Unseen Object Instance Segmentation via Long-Term Robot Interaction | RSS 2023 |
| Connecting the Brains via Virtual Eyes: Eye-Gaze Directions and Inter-brain Synchrony in VR | CHI 2021 |
| NFTree: Art Without Emissions | JIPP Vol. 2.4 |
Writing More
- Coq Tactics in Plain English
- A Brief Survey of Formal Models of Concurrency - arXiv Preprint
- The Verification of ARMv7 memset - Progress Report
- Theoretical Physics Notes
- Transcription of "Relativity: The Special and General Theory" by Albert Einstein - LaTeX source A nice quote from this book that I enjoyed - "No fairer destiny could be allotted to any physical theory, than that it should of itself point out the way to the introduction of a more comprehensive theory, in which it lives on as a limiting case."
- Interactive Object Segmentation in Mobile Robots - URSA Proposal December 2021
- A Brief Analysis of the Apollo Guidance Computer - arXiv Preprint - LaTeX source
Teaching
As an undergraduate, I taught two semester-long compiler design workshops, Practical Compiler Design in Spring 2023 and Introduction to Compiler Design in Fall 2023.
Additionally, I've given a number of educational outreach talks in fields such as formal verification and quantum computing through the UTD Computer Security Group (of which I am an officer) and the Dallas Hackers' Association.
Projects
Web Ring
| Site | Notes | |
|---|---|---|
| Software Languages Security Lab | ||
| Dr. Kevin Hamlen | Principal Investigator | |
| Ilan Buzzetti | Graduate Student | |
| Saquib Irtiza | Graduate Student | |
| TrustLab | ||
| Christophe Hauser | Principal Investigator | |
| Sergey Bratus | Principal Investigator | |
| Sean Smith | Principal Investigator | |
| Ben Kallus | Graduate Student | |
| Wei-Cheng Wu | Graduate Student | |
| Kyungtae Kim | Assistant Professor | |
| Jonah Weinbaum | Graduate Student | |
| UTD | ||
| Elliot Tarbet | CSG Officer | |
| Payton Harmon | Former CSG President | |
| Jerry Teng | Former CSG Officer | |
| Willie Chalmers III | ||
| Dent | ||
| Sidh Suchdev | ||
| Alex Bellon | ||
| Sasha Huang | ||
| Garrett Gu | ||
| Rocq | ||
| Benjamin Pierce | ||
| Andrew Appel | ||
| Adam Chlipala | ||
| Li-yao Xia | ||
| Pierre-Marie Pédrot | ||
| Joomy Korkut | ||
| Yves Bertot | ||
| Miscellaneous | ||
| nocoffei | ||
Games
Miscellaneous
- Interesting Rocq Problems
- My public keys
- My Bookshelf
- My Record Collection
- Where Have I Been?
- Transcriptions of "The International Library of Music" Public Domain Sheet Music
- 88x31 Button
- Laptop Stickers 8-17-2025
