Edit and verify

TL;DR

This paper proposes new methods to improve the performance of automated theorem provers in extended static checking by exploiting the incremental nature of code changes.

Contribution

It introduces two approaches and a comprehensive solution to enhance theorem prover efficiency during incremental static analysis.

Findings

Significant performance improvements demonstrated

Approaches effectively reduce verification time

Applicable to real-world static checking scenarios

Abstract

Automated theorem provers are used in extended static checking, where they are the performance bottleneck. Extended static checkers are run typically after incremental changes to the code. We propose to exploit this usage pattern to improve performance. We present two approaches of how to do so and a full solution.