Summary
Currently, I am a design verification engineer at Tenstorrent. Previously, I was an Undergraduate student in the Department of Computer Science at The University of Texas at Austin. At UT, I—supervised by Dr. Warren A. Hunt, Jr.—expanded and improved a formal model of the x86 ISA written in the ACL2 theorem prover to allow it to boot Linux. I wrote and defended my honors thesis on that work and further developed it during my internship at Intel, where I proved many theorems in ACL2 about the behavior of the model and the behavior of programs running on it. Prior to that, I was a full stack web developer, with experience in both PHP and Node based stacks.
Education
Bachelor of Science in Computer Science - University of Texas at Austin
Austin, TX • Aug 2022 - Dec 2024 | GPA: 3.9
Honors Thesis:
Booting a Linux Kernel Modified to Minimize Peripheral Requirements on the ACL2 Model of the X86 ISA
Relevant Coursework:
Advanced Computer Architecture
Computer Architecture
Computer Networks
Cryptography
Data Structures
Discrete Math
Honors Operating Systems
Programming for Performance
Theory of Computation
Individual Study Courses: (Supervised by Dr. Warren A. Hunt, Jr.)
Computer Science Honors Thesis
Undergraduate Reading and Research
Work Experience
Design Verification Engineer - Tenstorrent
Austin, TX • Jan 2025 - Present
Formal Verification Intern - Intel Corporation
Austin, TX • May 2024 - Aug 2024
- Contributed to the formal model of the x86 ISA written in ACL2.
- Proved theorems in ACL2 regarding the behavior of the model, with a particular focus on address translation using a new TLB (Translation Lookaside Buffer).
- Identified and fixed several bugs in the x86 model.
- Proved the correctness of an x86 program called "zeroCopy," which involved moving data within the virtual address space by modifying page tables.
- Thoroughly documented the changes made to the model, ensuring clarity and ease of understanding for future contributors.
- The work is now publicly available under a BSD style license as part of the ACL2 Community Books.
Undergraduate Research Assistant - UT Austin
Austin, TX (Remote) • May 2023 - Aug 2023
- Supervised by Dr. Warren A. Hunt, Jr.
- Expanded the formal model of the x86 ISA written in ACL2 to make it capable of booting a modified Linux kernel, including modeling timer and TTY peripherals, modeling interrupt and exception behavior, and implementing additional instructions.
- Worked toward being able to prove theorems about arbitrary x86 code using the ACL2 theorem prover.
- Continued work on this project as part of undergraduate research courses and defended an honors thesis on it.
Full Stack Developer - SIC Digital
Austin, TX (Remote) • Oct 2020 - Jul 2022
- Worked on More Pickups, a service used by organizations to manage picking up donated items from donors' homes.
- Designed and implemented a prototype microservice-based backend architecture.
- Worked with JavaScript, Express, and PostgreSQL on the backend and HTML, CSS, JavaScript, and React on the web-based frontend.
- Created a React Native-based cross-platform mobile app.
Web Developer - Freelance Work
Houston, TX • Jun 2016 - May 2022
- Worked on websites built with WordPress and Drupal content management systems.
- Used PHP, HTML, CSS, and JavaScript to add functionality that clients requested.
Projects
x86isa - Formal x86 ISA Model in ACL2
Extended x86isa, the most comprehensive formal model of the x86 ISA, which is implemented as an emulator in ACL2. Enhanced it to boot Linux by adding support for peripherals, interrupts, and exception handling. Developed cosimulation tools which use hardware accelerated virtualization via KVM for bug detection, added a TLB implementation for improved performance, and proved theorems about the impact of the TLB on address translation.
Source
|
Documentation
Technologies Used:
ACL2
Emulation
Formal Verification
KVM
Virtualization
x86 Assembly
Point - Location Based Social Network
Point is a social network that allows users to make posts that show to people nearby the location where the post was made for a duration of time. The backend is an API written in Python with Flask and an SQLite database. The client is a mobile app written in Dart with Flutter.
Technologies Used:
Dart
Flask
Flutter
Python
SQLite
libqsim - Quantum Circuit Simulator Library
A library for the simulation of quantum computers written in C++. Supports simulating arbitrary quantum circuits with arbitrary unitary quantum gates. It is GPU accelerated using ArrayFire.
Source
|
Examples
Technologies Used:
ArrayFire
C++
GPU
Quantum Computing
CHIP-8 Emulator
Implementation of a CHIP-8 virtual machine written in C++, with SFML for the graphics and Dear ImGui for the menus, complete with a debugger and disassembler for CHIP-8 programs.
Source
Technologies Used:
C++
Dear ImGui
SFML
References
Dr. Warren A. Hunt, Jr. — Professor, Department of Computer Science, University of Texas at Austin
Dr. Anna Slobodova — Former Sr. Principal Engineer, Intel Corporation
Contact information available upon request
Skills
Languages
ACL2
C
C++
CSS
HTML
Java
JavaScript
PHP
Python
SQL
Web Development
Apache
Bootstrap
Flask
Laravel
Nginx
Node.js
React
REST APIs
SQL
Vue
Technology
Docker
Git
Kubernetes
Linux
Virtual Machines
