Incremental Verification by SMT-based Summary Repair
Sepideh Asadi, Martin Blicha, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina · 2020
We present UPPROVER, a bounded model checker designed to incrementally verify software while it is being gradually developed, refactored, or optimized.In contrast to its predecessor, a SAT-based tool EVOLCHECK, our tool exploits first-order theories available in SMT solvers, offering two more levels of encoding precision: linear arithmetic and uninterpreted functions, thus allowing a trade-off between precision and performance.Algorithmically UPPROVER is based on the reuse and repair of interpolation-based function summaries from one software version to another.UPPROVER leverages treeinterpolation systems in SMT to localize and speed up the checks of new versions.UPPROVER demonstrates an order of magnitude speedup on large-scale programs in comparison to EVOLCHECK and HIFROG, a non-incremental bounded model checker.