UpProver


UpProver is a Bounded Model Checker for C that verifies program versions w.r.t a fixed property so that instead of analysing the full program over and over again, it implements an incremental BMC approach based on interpolation-based function summarization.  To guarantee algorithmic correctness of UpProver, it requires a specialization of Craig interpolants called tree interpolants to summarize functions as their behavior relevant to a property in a reusable, localized form.

UpProver is implemented in C++ and uses the interpolating SMT solver OpenSMT which is used for both satisfiability solving and interpolation for computing function summaries.

UpProver in contrast to its predecessor, SAT-based tool eVolCheck, exploits first-order theories available in SMT solvers, offering more levels of encoding precision thus allowing a trade-off between precision and performance. The tool operates on three levels of precision — LRA, EUF, and propositional logic (PROP).

UpProver has two phases: (i) bootstrapping, and (ii) incremental check. The bootstrapping phase is required when the old version or its function summaries are not available (e.g., for the initial version of the system). This enables the generation of the summaries if applicable.

In the incremental check, UpProver checks the validity of summaries of program P1 against the encodings of the function bodies of program P2. If necessary, summaries are repaired on the fly.

The current implementation of UpProver lives at https://github.com/usi-verification-and-security/upprover and the branch 'upprover' hosting the stable version of UpProver.
 

 

Publications:

  1. UpProver: Incremental Verification by SMT-based Summary Repair, Sepideh Asadi, Martin Blicha, Antti Hyvarinen, Grigory Fedyukovich, and Natasha Sharygina, FMCAD 2020 (Supplemental Material, PDF, slides5-minutes-videovideo)
  2. Farkas-Based Tree Interpolation, Sepideh Asadi, Martin Blicha, Antti Hyvarinen, Grigory Fedyukovich, and Natasha Sharygina, SAS 2020 (Supplemental Material, PDF, slides, video)