Joey Dodds

Research & Engineering

Since beginning formal methods work in 2008, I have fallen in love with the idea that we can use math to make software better than it has ever been before. I have spent much of that time both building tools for formal verification and applying them to real programs. I hope that one day I will be able to feel that the software that my life depends on is worthy of trust.

Background

Before starting at Galois in 2015, Joey was a Ph.D. candidate at Princeton University, working mainly on the VST project doing research around verifying C programs. At Princeton, Joey also researched a logic for conditional information flow, as a candidate method for analyzing information flow in the SPARK Ada toolkit.

During his work as a Master’s student at KSU, Joey worked on Guardol, a programming language for configuring guards, a hardware solution to cross domain security. Specifically, he worked on various analyses for checking the validity of Guardol programs. Joey also contributed to the Kiasan bounded symbolic execution engine, as part of the Sireum project.

Current Projects

Blog Posts