VeriFun's main system window is separated into 2 sub-windows, viz.
Data structures, procedures and lemmas of the actual program may be organized in program folders. Using the drag&drop-feature, program items may be rearranged in the Program Window and moved to or out of program folders. These arrangements are irrelevant for verification and for the system’s language parser.
The Program Menu provides commands
The Proof Menu provides commands
A proof tree is developed by
When applying a proof rule to a leaf of a proof tree, the system expands the proof tree at that leaf by computing the descendant nodes for the leaf according to the chosen proof rule. The descendant nodes created by some of the proof rules are computed by a first-order theorem prover, called the Symbolic Evaluator. This tool uses the hypotheses and induction hypotheses of a proof node sequent, the definitions of the data structures and procedures as well as the verified lemmas of the actual program for computing a symbolic evaluation. The Symbolic Evaluator is a completely automated tool on which the user has no influence, except to stop or to cancel the computation of a symbolic evaluation.
VeriFun provides several automated features:
The File Menu provides the usual commands to save and reload intermediate work and to open the Import Window for working with proof libraries. VeriFun supports three file formats:
Last update 2016-03-02