Tool Usage

UpProver Demo

How to use UpProver for verifying revisions of C programs (version1.c and version2.c)

Bootstrapping phase

Run UpProver to perform the initial bootstrapping check of the program, namely version1.c (parameter --bootstrapping):

$ ./upprover --logic qflra --bootstrapping  version1.c
--logic <logic> is to specify the theory. At the moment, the supported theories are qflra, qfuf, and prop represents LRA, EUF and Propositional logic respectively.
One may use the parameter --unwind <N> to specify the maximal number of unrolling of each loop.
If the bootstrapping phase is successful, summaries of the function calls of version1.c are stored in an external file called __summaries.
If the new revision of the code arrives, we can proceed with the incremental phase.
Summary formula in LRA encoding:

 

Incremental phase

 When the program is changed (version2.c), perform the summary validation as follows. Note that version2.c is a parameter of --summary-validation.

$ ./upprover  --logic qflra version1.c --summary-validation version2.c

This phase not only verifies the version2.c based on the result of the previous step, but also outputs a new __summaries file that is a repair of the previous summaries.

 

Tree-Interpolation Property (TIP)

To guarantee the soundness of incremental check in UpProver Tree-Interpolation Property (TIP) must be preserved in interpolation algorithm. In our work in SAS'20 we proved that Farkas interpolation algorithm guarantees the TIP and we showed that Decomposing Farkas interpolation algorithm guarantees TIP under a certain condition. We also showed that TIP is not guaranteed by dual Farkas, dual decomposing Farkas, and a flexible variant of Farkas interpolation algorithm. For those algorithms that TIP is not preserved, we can check the TIP of the computed summaries after bootstrapping phase. To this end, run TIP-check option as follows:

$ ./upprover  --logic qflra  --TIP-check version1.c


UpProver demo presented in SRI2021 summer school is available here.