Interactive Correctness Proofs for Software Modules Using KIV

This paper presents the KIV (Karlsruhe Interactive Verifier) proof environment for interactive, machine-supported verification of software modules with algebraic interface specifications. The aim is to make industrial-strength verification of software possible, and KIV is currently involved in industrial projects. We present the proof method, tactics, automated support, and the KIV proof engineering facilities for the development of correct software.