Title :
Interactive correctness proofs for software modules using KIV
Author :
Reif, Wolfgang ; Schellhorn, Gerhard ; Stenzel, Kurt
Author_Institution :
Abt. Programmiermethodik, Ulm Univ., Germany
Abstract :
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
Keywords :
algebraic specification; formal specification; program verification; KIV; KIV proof engineering facilities; Karlsruhe Interactive Verifier; algebraic interface specifications; industrial-strength verification; interactive correctness proofs; machine-supported verification; software modules; Application software; Banking; Computer industry; Construction industry; Data compression; Environmental economics; Power generation economics; Programming; Scalability; Transportation;
Conference_Titel :
Computer Assurance, 1995. COMPASS '95. Systems Integrity, Software Safety and Process Security. Proceedings of the Tenth Annual Conference on
Conference_Location :
Gaithersburg, MD
Print_ISBN :
0-7803-2680-2
DOI :
10.1109/CMPASS.1995.521894
