About Me

avatar

My name is Will Leeson. I’m a Ph.D. student at the University of Virginia studying under Matt Dwyer and a member of the LESS LAB. I’m originally from Tinley Park, a suburb of Chicago. I earned degrees in Computer Science and Data Analytics from Drake University. When I’m not working on research, I like to spend time with friends or doing one of my hobbies (if I’m lucky, both). These include playing music, cooking, board games, video games, and painting.

Research Interest

My research revolves around software verification. Software dominates the world. It’s important that any software that can affect people be proven safe. Software verification can prove that some program meets a specification set by the user. This is a hard problem that becomes harder the larger and more complex a codebase gets. I aim to make this problem a more practical one, whether that be through simplifying the problem or using the right tools for the right job.

Tools

  1. Graves-CPA - Graves-CPA is a verifier built on the CPAChecker framework. Given a C program and a specification, Graves-CPA uses graph neural networks to decide the ideal order in which to run a suite of verification algorithms to prove software safe.
  2. graph-builder - graph-builder is a tool which will take in a C program and generate a graph based on the program’s AST, control flow, and data flow. I have plans to expand it beyond just C programs.
  3. llama - llama is a tool developed by Mitchell Gerrard and myself to perform modular verification on functions inside a codebase. It produces files that can be verified by tools inside of alpaca.

Publications

Coming soon (hopefully)

References