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.

📄️ Functions, Axioms, and Domains

User-defined functions, both definitional and uninterpreted with equality (EUF).