Skip to main content

A Zoo of HeyVL Examples

Worked Examples​

  • Expected Runtime of a Geometric Loop. A short first example: use a supplied invariant to bound the expected number of loop iterations.
  • Lossy List Traversal. Define a list type and an exponential function, then verify a probability bound that depends on the list's length.
  • Induction and k-Induction. Compare invariants that are preserved by one loop iteration with those that require several iterations.
  • Almost-Sure Termination. Prove termination with probability one for a loop whose chance of exiting decreases as its counter grows.
  • Model Checking. Analyze a bounded geometric loop using Caesar's Storm backend, without supplying an invariant.

Example Collections​

The repository contains further HeyVL examples and tests, including examples for individual language features and proof rules. It also contains pGCL programs and their translations to HeyVL.