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.
Procedures are HeyVL's logical units of code.
Statements are executed sequentially and may have side-effects.
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.
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.