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.