Compiler Design for Automated Software Analysis Based on Optimization of Lyapunov Invariants

SHARE:

Compiler Design for Automated Software Analysis Based on Optimization of Lyapunov Invariants

Faculty Advisor: Mardavij Roozbehani
Mentor(s):
Contact e-mail: mardavij@mit.edu
Research Area(s): Computer Systems, Control, Theoretical Computer Science
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. See also here for a related article and links to related papers:
Link

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. The project builds on the previous work that developed a simple compiler for parsing and analysis of limited class of computer programs. We will be adding additional features both the compiler and to the analysis techniques to expand the class of programs and properties that can be verified.

Knowledge of compiler design is a must, familiarity with convex optimization and the associated software packages such as Sedumi and Yalmip is a plus.

See more projects

Return to the SuperUROP site.