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
- Contact:
German Research Center for Artificial Intelligence GmbH
W. Stephan
Stuhlsatzenhausweg 3
66123 Saarbruecken
Germany
stephan@dfki.uni-sb.de
University of Ulm
Fakultaet fuer Informatik
Abt. Programmiermethodik und Compilerbau
W. Reif
Oberer Eselsberg
89069 Ulm
Germany
reif@informatik.uni-ulm.de
- Line Count: >= 70,000
- Number of Users: >= 25
- Number of Sites: >= 15 (industry and research institutions)
- Language: PPL
- Availability: Contact developer at above address.