HeyVL

HeyVL is a verification language similar to Viper and Boogie. The main innovation is that it supports quantitative reasoning via its constructs inspired by Gödel logic. Refer to our publications for details on the theory.

A HeyVL file consists of a sequence of declarations: procedure and domain declarations. Refer to those for more information.

📄️ Procedures

Procedures are HeyVL's logical units of code.

📄️ Statements

Statements are executed sequentially and may have side-effects.

📄️ Expressions

HeyVL's expressions evaluate to a value in a state.

📄️ Domains, Uninterpreted Functions, and Axioms

Domain blocks are used to create user-defined types and uninterpreted functions.