Incremental Verification by SMT-based Summary Repair

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 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.

BibTeX:

@inproceedings{asadi_incremental_2020,
    title = {{Incremental Verification by SMT-based Summary Repair}},
    author = {Asadi, Sepideh and Blicha, Martin and Hyvärinen, Antti E. J. and Fedyukovich, Grigory and Sharygina, Natasha},
    year = {2020},
    booktitle = {{Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design -- FMCAD 2020}},
    editor = {Ivrii, Alexander and Strichman, Ofer},
    publisher = {TU Wien Academic Press},
    series = {{Formal Methods in Computer-Aided Design}},
    doi = {10.34727/2020/isbn.978-3-85448-042-6},
    isbn = {978-3-85448-042-6},
}

Proceedings paper