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

Publications: