Interactive correctness proofs for software modules using KIV
- 19 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
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
This publication has 10 references indexed in Scilit:
- Correctness of generic modulesPublished by Springer Nature ,2005
- Reuse of proofs in software verificationPublished by Springer Nature ,1993
- The KIV system: Systematic construction of verified softwarePublished by Springer Nature ,1992
- Verification of large software systemsPublished by Springer Nature ,1992
- Tactical theorem proving in program verificationPublished by Springer Nature ,1990
- HOL: A Proof Generating System for Higher-Order LogicPublished by Springer Nature ,1988
- A compiler for conditional term rewriting systemsPublished by Springer Nature ,1987
- Hierarchical program specification and verification ? a many-sorted logical approachActa Informatica, 1980
- Edinburgh LCFLecture Notes in Computer Science, 1979
- First-Order Dynamic LogicLecture Notes in Computer Science, 1979