Specification and Verification of Software

KIV (Karlsruher Interactive Verifier) is the name of a verification tool implemented in LISP. A program, written in a PASCAL-like language, is seen to be correct iff it meets its algebraic specification expressed in the tradition of abstract datatypes (ADT). The KIV proofs stating the correctness of a program are written in terms of a suitable Dynamic Logic and have mainly to be constructed interactively by the KIV user. KIV was developed under the leadership of Prof. Menzel at the University of Karlsruhe beginning in 1986. Since 1994 resp. 1996, other groups at the DFKI Saarbrücken and at the universities in Ulm/Augsburg have continued developing own extensions of KIV. At the University of Karlsruhe the development of KIV was abandoned to make the development of the new KeY system possible. For the same reason, the websites of KIV at Karlsruhe are outdated and should be seen as archive material documenting former activities.

KIV
KIV (Karlsruher Interactive Verifier) is the name of a verification tool implemented in LISP. A program, written in a PASCAL-like language, is seen to be correct iff it meets its algebraic specification expressed in the tradition of abstract datatypes (ADT). The KIV proofs stating the correctness of a program are written in terms of a suitable Dynamic Logic and have mainly to be constructed interactively by the KIV user. KIV was developed under the leadership of Prof. Menzel at the University of Karlsruhe beginning in 1986. Since 1994 resp. 1996, other groups at the DFKI Saarbrücken and at the universities in Ulm/Augsburg have continued developing own extensions of KIV. At the University of Karlsruhe the development of KIV was abandoned to make the development of the new KeY system possible. For the same reason, the websites of KIV at Karlsruhe are outdated and should be seen as archive material documenting former activities.
KeY
Since 1998, a new-generation verification tool has been developed in the context of the KeY project which is headed by Prof. W.Menzel, Prof. P.H.Schmitt, and Prof.Hähnle and supported by Deutsche Forschungsgemeinschaft (DFG). The project aims to encourage the use of formal methods for software development. The way to reach this goal is by seamless integration of formal methods in heavily used CASE tools. Prior to integration, however, one has to unify the formalisms used when developing and verifying software. Both unification of formalisms and integration into a commercial CASE tool are research topics in the KeY project. The logical foundation is -- as for the KIV system before -- an intuitive Dynamic Logic; now tuned to handle with programs written in JavaCard and with specifications given in UML/OCL.