KIV is a tool for formal systems development and interactive verification. It can be employed, e.g.,
- for the development of safety critical systems from formal requirements specifications down 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 down to a verified compiler,
- for building security models and architectural models as they are needed for high level ITSEC or CC evaluations.
The homepage has been moved to isse.de