MIT EECS - VMware Undergraduate Research and Innovation Scholar
Compiler Design for Automated Software Analysis Based on Optimization of Lyapunov Invariants
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.