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.

📄️ 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.

Use the source, Luke

We do not formally describe the syntax of HeyVL in this documentation. You can find a more formal definition in the src/front/parser/grammar.lalrpop file that specifies the syntax used to generate Caesar's parser. It is written in the LALRPOP language.

Examples

The pgcl/examples-heyvl directory contains the machine-translated HeyVL code for our pGCL examples. Note that they are just sequences of HeyVL statements without wrapping procedure declarations. Refer to the page on the pGCL frontend for more information.

Caesar's integration tests in tests/ can also serve as a reference. Refer to the development guide for more information about these tests.