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.
- Developers: M. Heisel, B. Langenstein, W.Reif, G. Schellhorn,
K. Stenzel, W. Stephan, A. Wolpers,
and dozens of students
German Research Center for Artificial Intelligence GmbH
University of Ulm
Fakultaet fuer Informatik
Abt. Programmiermethodik und Compilerbau
- Line Count: >= 70,000
- Number of Users: >= 25
- Number of Sites: >= 15 (industry and research institutions)
- Language: PPL
- Availability: Contact developer at above address.