Abstract
KIV is a tool for formal systems development. It can be employed, e.g.,
-
—
for the development of safety critical systems from formal requirements specifications to executable code, including the verification of safety requirements and the correctness of implementations,
-
—
for semantical foundations of programming languages from a specification of the semantics to a verified compiler,
-
—
for building security models and architectural models as they are needed for high level ITSEC [7] or CC [1] evaluations.
Chapter PDF
References
CCIB-98-026. Common Criteria for Information Technology Security Evaluation, Version 2.0. ISO/IEC JTC 1, May 1998. available at http://www.csrc.nist.gov/cc.
CoFI: The Common Framework Initiative. Casl — the CoFI algebraic specification language tentative design: Language summary, 1997. Available at http://www.brics.dk/Projects/CoFI.
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, LNCS 894, Berlin, 1994. Princeton (USA), Springer. http://www.informatik.uni-bremen.de/~davinci/.
G. Schellhorn. Verifikation abstrakter Zustandsmaschinen. PhD thesis, Universität Ulm, Fakultät für Informatik, 1999. (to appear, in German).
Y. Gurevich and J. Huggins. The semantics of the c programming language. In E. Börger, H. Kleine Büning, G. Jäger, S. Martini, and M.M. Richter, editors, Computer Science Logic. Springer LNCS 702, 1993.
D. Harel. First Order Dynamic Logic. LNCS 68. Springer, Berlin, 1979.
ITSEC. Information Technology Security Evaluation Criteria, Version 1.2. Office for Official Publications of the European Communities, June 1991.
S. Kaplan. A compiler for conditional term rewriting systems. In 2nd Conf. on Rewriting Techniques and Applications. Proceedings. Bordeaux, France, Springer LNCS 256, 1987.
W. Reif. The KIV-approach to Software Verification. In M. Broy and S. Jähnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software — Final Report, LNCS 1009. Springer, Berlin, 1995.
W. Reif, G. Schellhorn, and K. Stenzel. Interactive Correctness Proofs for Software Modules Using KIV. In COMPASS’95 — Tenth Annual Conference on Computer Assurance, Gaithersburg (MD), USA, 1995. IEEE press.
W. Reif, G. Schellhorn, K. Stenzel, and M. Balser. Structured specifications and interactive proofs with KIV. In W. Bibel and P. Schmitt, editors, Automated Deduction — A Basis for Applications. Kluwer Academic Publishers, Dordrecht, 1998.
W. Reif and K. Stenzel. Reuse of Proofs in Software Verification. In R. Shyamasundar, editor, Foundation of Software Technology and Theoretical Computer Science. Proceedings, LNCS 761, pages 284–293, Berlin, 1993. Bombay, India, Springer.
G. Schellhorn and W. Ahrendt. Reasoning about Abstract State Machines: The WAM Case Study. Journal of Universal Computer Science (J.UCS), 3(4):377–413, 1997. Available at http://www.hyperg.iicm.tu-graz.ac.at/jucs/.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A. (2000). Formal System Development with KIV. In: Maibaum, T. (eds) Fundamental Approaches to Software Engineering. FASE 2000. Lecture Notes in Computer Science, vol 1783. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46428-X_25
Download citation
DOI: https://doi.org/10.1007/3-540-46428-X_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67261-6
Online ISBN: 978-3-540-46428-0
eBook Packages: Springer Book Archive