Title: Design and Evaluation of Incrementalization in SpaceSearch
Advisors: Zach Tatlock and Michael Ernst
Abstract: SpaceSearch is a library for building solver-aided verification tools within a proof assistant, allowing a user to verify the tools according to semantics defined in Coq and, using Coq's extraction facilities, produce an implementation of this solver-aided tool in Rosette. This allows a user to formally prove the correctness of the domain-specific reductions and optimizations that are commonly used to reduce the search space for a solver-aided tool and make more efficient use of the SMT solver's capabilities. In this talk, I will discuss my contributions to the design and evaluation of SpaceSearch, particularly the semantics and implementation of incrementalization, which allows for tools produced by SpaceSearch to avoid searching portions of a space that they had previously searched. I will also discuss design challenges when using SpaceSearch and possible areas of further exploration, as in the case of attempting to incorporate SpaceSearch's incrementalization feature into Bagpipe, a solver-aided BGP configuration checker built and verified in SpaceSearch.