Cuv\'ee: Blending SMT-LIB with Programs and Weakest Preconditions

TL;DR

Cuvée is a program verification tool that extends SMT-LIB input with weakest precondition operators, translating them into first-order SMT for easier analysis and synthesis, notably reducing annotation effort for loop verification.

Contribution

Cuvée introduces a novel input format combining SMT-LIB with weakest preconditions and employs symbolic execution to lower annotation requirements in loop verification.

Findings

Successfully translates extended SMT-LIB inputs into first-order SMT.

Reduces annotation burden by using pre-/postconditions instead of invariants.

Facilitates tool unification for program synthesis and verification.

Abstract

Cuv\'ee is a program verification tool that reads SMT-LIB-like input files where terms may additionally contain weakest precondition operators over abstract programs. Cuv\'ee translates such inputs into first-order SMT-LIB by symbolically executing these programs. The input format used by Cuv\'ee is intended to achieve a similar unification of tools for that for example synthesize loop summaries. A notable technical aspect of Cuv\'ee 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.