My current research is focused on symbolic representations of points-to analyses.

This project was done in collaboration with Dr. Thomas Ball and Dr. Ella Bounimova during my internship at Microsoft Research.

The main goal of this work was to improve the BEBOP model checking engine. BEBOP is a part of SLAM, a tool used for device driver verification. SLAM performs a counter-example guided abstraction refinement (CEGAR), producing increasingly refined versions of a program in each iteration. Our hypothesis was that reachability analysis could reuse information computed in the previous steps. To test the hypothesis, we devised an incremental algorithm for symbolic reachability analysis of Boolean programs. We implemented the algorithm as a prototype extension of the BEBOP model checker.

I have implemented the difference logic theory solver in the framework of OpenSMT with the help of Roberto Bruttomesso. We experimented with different ways to do theory propagation in the context of difference logic.

The project was based on an extension of logic of word equations, called buffer logic, devised by Prof. Natasha Sharygina and Dr. Stefano Tonetta.

I have developed a generator for buffer logic formulas (verification conditions) for programs described in a subset of C. To facilitate experiments with different expressiveness-performance tradeoffs I have developed a suitable intermediate representation.