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
Abstract

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.