@inproceedings{zhou2024context,
author = {Zhou, Yi and Bosamiya, Jay and Li, Jessica and Heule, Marijn and Parno, Bryan},
title = {Context Pruning for More Robust SMT-based Program Verification},
booktitle = {Formal Methods in Computer-Aided Design (FMCAD)},
year = {2024},
month = {October},
abstract = {SMT solvers provide powerful proof automation for program verification. However, relying on SMT solvers also leads to proof instability, where a previously successful proof may fail after the developer makes trivial modifications to the source program. Such instability is a major headache for developers, but the causes and potential mitigations for it have received limited attention. In this study, we find that irrelevant query context accounts for 78% of the instability in existing program-verification query sets. As a result, we design SHAKE, a novel technique that leverages the structure in program-verification SMT queries in order to filter out irrelevant context from such queries. SHAKE is the first SMT-level technique that targets instability, and we implement it as a pre-processing step for SMT solvers. We evaluate SHAKE on real-world, large-scale query sets, and we find that it leads to large reduction in context and a 29% and 41% improvement in query stability on Z3 and cvc5, with minor performance overhead.},
url = {http://approjects.co.za/?big=en-us/research/publication/context-pruning-for-more-robust-smt-based-program-verification/},
}