Kenneth Siebert
MIT EECS - Draper Undergraduate Research and Innovation Scholar
Compiler Design for Automated Software Analysis Based on Optimization of Lyapunov Invariants
2013–2014
Mardavij Roozbehani
The goal of this project is to develop new tools based on systems and control theory for verification of a specific subset of numerical software systems. This would enable us to detect run time errors on a specific set of programs before running them. For implementation, our project aims to develop a compiler that can take an input, which is limited to a subset of C programs, and output a higher-level model of the program to be used for verification purposes. The verification process of the higher–level model is rooted in Lyapunov Invariants theory and convex optimization. The project aims to verify software against some specific run time errors such as overflow, infinite loops and divide by zero errors, as well as user defined assertions. This compiler design and implementation is under way and an intermediate model can already be produced by the compiler. This project aims to complete the compiler and potentially add new features to be able to verify a broader set of programs.
Over the past summer, I worked at Serendipity a big data startup on creating a communication layer for our distributed systems responsible for providing real time data visualizations to our users.”