|Incremental symbolic reachability for Boolean programs
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.