Karlsruhe Interactive Verifier (KIV)

KIV is an interactive theorem prover with a user definable object logic. The main applications rely on a definition of dynamic logic, for reasoning about the correctness of software systems. Several other object logics have been defined for experimental pursoses.

The core of KIV is implemented in an ML-like functional language called PPL, and interfaces to the outside world via yacc/lex generated parsers and C/Motif. PPL itself is implemented in Lisp.

KIV is used, among others, in the Verificaiton Support Environment (VSE) developed for the German Information Security Agency. For this pursose, KIV was integrated with an induction theorem prover and a case tool.