Worked with Professor Stephen Edwards at Columbia University to add Z3’s SMT framework to an existing compiler project in order to resolve variable bit widths at compile time.

Abstract

SMT solvers have, in recent years, undergone optimizations that allow them to be considered for use in commercial software. Usages for such SMT solvers include program verification, buffer overflow detection, bit-width prediction, and loop unrolling. Companies such as Microsoft have pioneered SMT research through their Z3 solver. In this paper I investigate the potential techniques for implementing these techniques as well as provide examples of potential applications of SMT solvers.

paper