Command: ivy

This command runs an interactive user interface for constructing inductive invariants. The options are as follows:

ui=interface

Here, interface specifies the user interface for invariant construction. The values are:

• art This interface supports interactive construct of an Abstract Reachability Tree.
• cti This interface supports an interactive approach to invariant construction based on counterexamples to induction.

The default value is art.