ISSE

Search

Interactive Correctness Proofs for Software Modules Using KIV

W. Reif, G. Schellhorn, and K. Stenzel

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.
published 1995 in: USA COMPASS'95 - Tenth Annual Conference on Computer Assurance, Gaithersburg (MD)

Publisher: IEEE press


Downloads: