Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Abadi, M. Burrows, B. Lampson, and G. Plotkin. A Calculus for Access Control in Distributed Systems. In J. Feigenbaum, editor, CRYPTO '91. Springer LNAI 576, 1991.
Egon BŐrger and Dean Rosenzweig. A mathematical definition of full PROLOG. Science of Computer Programming, 1994.
T. Fuchß, W. Reif, G. Schellhorn, and K. Stenzel. Three Selected Case Studies in Verification. In M. Broy and S. Jährlichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software — Final Report. Springer LNCS 1009, 1995.
M. Fröhlich and M. Werner. Demonstration of the interactive graph visualization system davinci. In R. Tamassia and I. Tollis, editors, DIMACS Workshop on Graph Drawing '94. Proceedings, Springer LNCS 894. Princeton (USA), 1994.
S. Kaplan. A compiler for conditional term rewriting systems. In 2nd Conf. on Rewriting Techniques anf Applications. Proceedings. Bordeaux, France, Springer LNCS 256, 1987.
W. Reif. The KIV-approach to Software Verification. In M. Broy and S. Jährlichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software — Final Report. Springer LNCS 1009, 1995.
W. Reif and K. Stenzel. Reuse of Proofs in Software Verification. In J. Köhler, editor, Workshop on Formal Approaches to the Reuse of Plans, Proofs, and Programs. Montreal, Quebec, 1995.
W. Reif, G. Schellhorn, and K. Stenzel. Interactive Correctness Proofs for Software Modules Using KIV. In Tenth Annual Conference on Computer Assurance, IEEE press. NIST, Gaithersburg, MD, USA, 1995.
G. Schellhorn and W. Ahrendt. Verification of a Prolog Compiler — First Steps with KIV. Ulmer Informatik-Berichte 96-05, Universität Ulm, Fakultät für Informatik, 1996.
D. T. Sanella and M. Wirsing. A kernel language for algebraic specification and implementation. In Coll. on Foundations of Computation Theory, Springer LNCS 158. Linköping, Sweden, 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Reif, W., Schellhorn, G., Stenzel, K. (1997). Proving system correctness with KIV. In: Bidoit, M., Dauchet, M. (eds) TAPSOFT '97: Theory and Practice of Software Development. CAAP 1997. Lecture Notes in Computer Science, vol 1214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0030647
Download citation
DOI: https://doi.org/10.1007/BFb0030647
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62781-4
Online ISBN: 978-3-540-68517-3
eBook Packages: Springer Book Archive