Cuv\'ee: Blending SMT-LIB with Programs and Weakest Preconditions
2020
academicJournal
Zugriff:
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.
Titel: |
Cuv\'ee: Blending SMT-LIB with Programs and Weakest Preconditions
|
---|---|
Autor/in / Beteiligte Person: | Ernst, Gidon |
Link: | |
Veröffentlichung: | 2020 |
Medientyp: | academicJournal |
Schlagwort: |
|
Sonstiges: |
|