An introduction to K Lab (developed by DappHub)

This video demonstrates how to use the KLab tool developed by DappHub.

The KLab tool interactively explores execution traces produced by the K Framework when executing a given proof obligation. You can explore the execution trace using `n` and `p` (for next and previous state), `Shift n` and `Shift p` (finer grained next and previous state), and `Control n` and `Control p` (coarser grained next and previous state). Several views are supported, including the `b`ehavior view (turned on with `b`), the `e`vm view, the `c`onstraint view, and the `k`-cell view.

Below you'll find resources for getting support for both KLab and the K Framework:

[caseydetrio]

At 14:30, the field `extraReqs` is deleted and the property below it is moved to the field `requires`. extraReqs is just a garbage name which effectively comments out the property below.