Skip to content
View CharlesAverill's full-sized avatar
👽
Klaatu Barada Nikto
👽
Klaatu Barada Nikto

Block or report CharlesAverill

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
CharlesAverill/README.md

Howdy!

My name is Charles Averill, I'm a Computer Science PhD student at the University of Texas at Dallas under Kevin Hamlen and Christophe Hauser. I graduated from UTD with a Bachelor's degree in Computer Science and a minor in Physics. Now I study formal verification, with interests in proof automation via stronger tactics, pure type theory, user-friendly verification, safe program transformations, formalized physics, invariant generation, etc.

Check my profile pins for some of my favorite projects, or you can go to my homepage to see a bunch of other stuff.

ORCID iD icon https://orcid.org/0000-0001-6614-1808

What I'm currently working on

As of December 2024, I have started my Ph.D. in Computer Science (focused in Formal Verification) at the University of Texas at Dallas, where I am coadvised by Dr. Kevin Hamlen and Dr. Christophe Hauser at Dartmouth College. This semester I've largely studied properties of time, specifically the timing properties of machine code at a formal level under my lab's framework for formal verification of machine code, Picinae. Additionally, I've taken an interest in concurrency and Separation Logic - read the short survey paper I wrote on Formal Models of Concurrency for my Computer Networks course. With the large time commitment of starting a Ph.D. I've had little time to work on personal projects like I used to, but in the little free time I've had I've worked on some more of Software Foundations, some projects for my networking course featuring networking protocols in OCaml and Coq, and an addition to my website that invites friends to watch what I listen to on Spotify.

Previous
May 2024

As of May 2024, I recently accepted my offer of admission to the Computer Science Ph.D. program at the University of Texas at Dallas, where I will be studying under Dr. Kevin Hamlen. I submitted VOLPIC to the PLDI 2024 Student Research Competition, which has just been accepted! This summer I will travel to Copenhagen to present the research. Since mid-February, I've been solo traveling through Italy, Croatia, and Greece. I've had a wonderful time exploring these countries, and I'm disappointed that my journey will be finished in only a few more weeks. Keep an eye out for the inevitible blog post I'll be writing about the trip. In my free time, I've been studying formal verification by continuing to work through the Software Foundations series, a project that I also recently joined as a contributor. I've also continued to tinker on a decompilation hack of Pokemon FireRed that I pick up every few years, a very relaxing pastime.

February 2024

As of February 2024, I recently graduated with my Bachelor's degree in Computer Science with a minor in Physics! I've also submitted my applications for Formal Verification Ph.D. programs at Carnegie Mellon University, Cornell University, The University of Pennsylvania, The University of Washington, MIT, and Oxford University, still waiting on results from each. For the past month I've worked on a few projects, most notably VOLPIC, a formal verification platform for the Pascal programming language using Coq. I gave this presentation at the Dallas Hackers Association on my progress. In addition to writing code, I've been preparing for my upcoming trip to the Mediterranean by continuing to study Greek (I'm on month 7) and catch up on Italian. I made this page to keep track of phrases I'd like to remember. I've also started to play Chess again, add me on Chess.com!

September 2023

As of September 2023, I recently attended IEEE Quantum Week 2023 on scholarship from the NSF. I'm currently applying for graduate CS programs at schools like CMU, UPenn, UW, and Oxford. I'm continuing my research with Dr. Kevin Hamlen on bottom-up verification of binary programs. I'm working on NAME, a language-agnostic, modular assembly language emulation pipeline as my senior capstone project, I'm teaching the second iteration of my Introduction to Compiler Design course, and I started playing Go. Send me a challenge!

July 2023

As of July 2023, I recently attended PLDI 2023 and presented my poster for Prettybird at the Student Research Competition. I'm interning at NVIDIA on the Linux Graphics Testing team for the second time, and I'm researching with Dr. Kevin Hamlen on bottom-up verification of binary programs. I'm refining the curriculum for my Practical Compiler Design course for the Fall 23 semester, and I'm ramping up to apply for graduate school for the 2024-2025 school year.

March 2023

As of March 2023, I have just submitted an extended abstract of Prettybird to the PLDI 2023 Student Research Competition. I began teaching my Practical Compiler Design course this semester, and it's going strong. I'll be presenting a talk on Formal Program Verification at the first Dallas Cyberfest soon.

November 2022

As of November 2022, I have just finished working on Prettybird, a functional programming language for font generation. I submitted a paper for this project to PLDI 2023 and am waiting to hear back.

I am preparing to teach a course in practical compiler design next semester to a tentative 50 students, the code and lectures for this course will be public soon.

Summer 2022

As of Summer 2022, I am working on Ocarina of Time: Legendary Edition, a decompilation hack of OOT intended to add story elements (and whatever else I want) from the OOT manga. It's been tons of fun, and the decomp is still in the early documentation phase, so it's like trekking through a jungle most of the time.

I'm also planning on revisiting Purple, I have a few ideas of how to go about it and I'm excited to revisit.

April 2022

As of April 2022, I am in between a few projects. YARR is now a fully-functional (and mostly realtime) raytracing renderer written in CUDA C/C++. This project was incredibly fun, I strongly recommend a rendering project to anyone. I'm studying relativity with the intent to add relativistic rendering to the project, with the end goal of drawing some black holes.

I'm also working on a 3D remake of atc, a very addicting terminal game I've been playing instead of paying attention in class.

October 2021

As of October 2021, I am currently working on Purple, a simple compiled language! I'm learning a lot more about assembly and compiler design, and it's a lot of fun designing your own programming language!

Ask me about

My research! I've been researching at various laboratories and about various topics since 2020, and I always enjoy talking about the projects I worked on. Here's the list of publications I've worked on (more to come) -

How to reach me

Discord - @caverill_ formerly @caverill_1729

LinkedIn - https://linkedin.com/in/charles-averill

Pronouns

He/They

Fun Fact

Check out my music!


Charles's GitHub stats Top Languages

Pinned Loading

  1. volpic volpic Public

    Verifier of Lifted Pascal in Coq

    OpenEdge ABL 3

  2. zenith zenith Public

    A wireframe renderer written in OCaml

    OCaml 20

  3. prettybird prettybird Public

    Python 7 2

  4. yarr yarr Public

    Yet Another Relativistic Renderer

    Cuda 12

  5. aftn aftn Public

    A C implementation of Alien: Fate of the Nostromo, a 2021 board game of the same name

    C 19 1

  6. radio.charles.systems radio.charles.systems Public

    Website to track my spotify listening behavior

    Python