Abstrakt
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 uninter- preted 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 EVOLCHECK and HIFROG, a non-incremental bounded model checker.