The User Interface of the KIV Verification System - A System Description

This article describes the sophisticated graphical user interface (GUI) of the KIV verification system. KIV is a verification system that works on structured algebraic specifications. The KIV GUI provides means for developing and editing structured algebraic specifications and for developing proofs of theorems. The complete development process is performed through the GUI. For editing the specification files XEmacs is used, and for the management of the structured algebraic specifications we use daVinci, an extendable graph drawing tool which has been integrated into the KIV user interface. As proving is the most time-consuming part of formal verification, the most important part of the KIV GUI is our user interface for proof development. The proof is represented as a tree and can be manipulated through context menus. The main proof work is done in a proof window where the sequent of the current goal, the applicable rules and the main menu are displayed. Which rules are applicable depends on the current goal. KIV also supports the context-sensitive application of proof rules.