The goal of this project is to automate the process of software verification (i.e., proving that a given computer program does not produce run-time errors) for a limited class of software. The theoretical framework for finding certificates of safety for a high-level model of a program (e.g., a graph model) based on convex optimization techniques already exists. The main task in this project involves building a compiler which takes a structured class of software (e.g. a limited subset of c codes) as input, and produces a high level model (e.g., a graph model) that can be analyzed in an optimization-based framework. Building this compiler will allow us to verify the underlying concepts by providing a working framework for software verification.

I interned at Optiver US in Chicago, IL, working on software for low-latency trading systems. I worked at The Boeing Company in St. Louis, MO as a software developer intern. I completed an internship at Osram OS in Regensburg, Germany, developing software to test white LED lights.