Incremental Verification by SMT-based Summary Repair

TitleIncremental Verification by SMT-based Summary Repair
Publication TypeConference Paper
Year of Publication2020
AuthorsAsadi, Sepideh, Blicha Martin, Hyvärinen Antti E. J., Fedyukovich Grigory, and Sharygina Natasha
Conference NameFMCAD'20
PublisherIEEE 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.