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

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

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2020-10
Main Author: Ernst, Gidon
Format: Article
Language:English
Subjects:
Annotations
Program verification (computers)
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422