The functional approach uses higher-order algebraic specifications. The first-order part is a subset of CASL. Specifications are built up from elementary specifications with the operations enrichment, union, renaming, parameterization and actualization. Specifications have a loose semantics and may include generation principles to define inductive data types.

?

For the state-based approach KIV offers four approaches: Abstract State Machines (ASMs), parallel programs, and the direct verification of sequential Java programs (including generics).

?

ASMs define rules (abstract sequential programs that are executed atomically) to describe state transitions. The semantics of an ASM is the set of traces generated by the transition relation defined by the rules of the ASM. Our variant of ASMs is based on algebraically specified data types. The abstract programs used to define rules used include parallel assignments, (infinite) nondeterminism (with choose) and mutually recursive procedures.

Parallel programs extend the sequential ones with additional operators to execute programs in parallel, using shared variables: both (weak-fair and unfair) interleaving as well as asyncronous parallel execution are supported. An await-operator is used for synchronisation.

In KIV, formal specifications of software and system designs are represented explicitly as directed acyclic graphs called development graphs. Each node corresponds to a specification component or an ASM. Each node has a theorem base attached. Theorem bases initially contain axioms, ASM rules, and parallel programs and automatically generated proof obligations for refinements. The theorem base also stores theorems added by the user (proved and yet unproved ones), and manages proofs and their dependencies.

?

Frequently, the problem in engineering high assurance systems is not to verify proof obligations affirmatively, but rather to interpret failed proof attempts that may indicate errors in specifications, programs, lemmas etc. Therefore, KIV offers a number of proof engineering facilities to support the iterative process of (failed) proof attempts, error detection, error correction and re-proof. Dead ends in proof trees can be cut off, proof decisions may be withdrawn both chronologically and non-chronologically. Unprovable subgoals can be detected by automatically generating counter examples. This counter example can be traced backwards through the proof to the earliest point of failure. Thereby the user is assisted in the decision whether the goal to prove is not correct, proof decisions were incorrect, or there is a flaw in the specification. After a correction the goal must be re-proved. Here another interesting feature of KIV, the strategy for proof reuse, can be used. Both successful and failed proof attempts are reused automatically to guide the verification after corrections. This goes far beyond proof replay or proof scripts. We found that typically 90% of a failed proof attempt can be recycled for the verification after correction.

?

The correctness management in KIV ensures that changes to or deletions of specifications, modules, and theorems do not lead to inconsistencies, and that the user can do proofs in any order (not only bottom up). It guarantees that only the minimal number of proofs are invalidated after modifications, that there are no cycles in the proof hierarchy and that finally all used lemmas and proof obligations are proved (in some sub-specification).

?

KIV offers a powerful graphical user interface (see this paper) which has been constantly improved over the years. The intuitive user interface allows easy access to KIV for first time users, and is an important prerequisite for managing large applications. The interface is object oriented, and is implemented in Java to guarantee platform independency.

?

The top-level object of a development, the development graph, is displayed graphically (an example is above). The theorem base, which is attached to each development node, is arranged in tables, and context sensitive popup menus are provided for manipulation. While proving a theorem, the user is able to restrict the set of applicable tactics by selecting a context, i.e. a formula or term in the goal, with the mouse. This is extremely helpful for applying rewrite rules, as the set of hundreds of rewrite rules is reduced to a small number of applicable rules for the selected context. Proofs are presented as trees, where the user can click on nodes to inspect single proof steps.

?

In large applications, the plentitude of information may be confusing. Therefore, important information is summarized, and more details are displayed on request. Different colors are used to classify the given information. A special font allows the use of a large number of mathematical symbols.

?

KIV automatically produces LaTeX as well as XML documentation for a development on different levels of detail (see the KIV projects page for various examples of the latter). Specifications, implementations, theorem bases, proof protocols, and various kinds of statistics are pretty printed. The user is encouraged to add comments to specifications, which are also used to automatically produce a data dictionary. As several users may work simultaneously on a large project, the documentation facilities of KIV are very important. The automatically extracted information can also be included into reports.