Cuvée: Blending SMT-LIB with Programs and Weakest Preconditions

10/10/2020

∙

by   Gidon Ernst, et al.

∙

0

∙

share

Cuvée is a program verification tool that reads SMT-LIB-like input files where terms may additionally contain weakest precondition operators over abstract programs. Cuvée translates such inputs into first-order SMT-LIB by symbolically executing these programs. The input format used by Cuvée is intended to achieve a similar unification of tools for that for example synthesize loop summaries. A notable technical aspect of Cuvée itself is the consequent use of loop pre-/postconditions instead of invariants, and we demonstrate how this lowers the annotation burden on some simple while programs.