|Title||Incremental Verification by SMT-based Summary Repair|
|Publication Type||Conference Paper|
|Year of Publication||2020|
|Authors||Asadi, Sepideh, Blicha Martin, Hyvärinen Antti E. J., Fedyukovich Grigory, and Sharygina Natasha|
|Publisher||IEEE digital library|
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 tree-interpolation 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 non-incremental verification and to EVOLCHECK.