- Suche

- Kontakt

The KIV System


KIV is a tool for formal systems development and interactive verification. It can be employed, e.g.,

Special care was (and is) taken to provide strong proof support for all validation and verification tasks. KIV can handle large scale formal models by efficient proof techniques, multi-user support, and an ergonomical user interface. It has been used in a number of industrial pilot applications, but is also useful as an educational tool for formal methods courses.

KIV has recently been ported to the Scala programming language and integrated into the Eclipse platform as a plugin.


Overview Paper

Quick Start

Project Gallery

Documentation (pdf).


  • June 14/15 2014 We're participating at the Verified Software Competition (VSCOMP) 2014. The submitted solutions can be found here

  • June 2014 The new Scala version of KIV is available!

    Feel free to try it out. This version has already replaced the old system for most of our internal use. However, there are many minor issues with the system, in particular, error reporting needs improvement and the documentation is not up-to-date. Don't hesitate to contact us if you have questions.

  • April 2014 The report from the VerifyThis Competition at FM 2012 is published


KIV comes as an Eclipse plugin which you can download from the update site listed below. The plugin depends on parts of the Scala IDE for Scala 2.11, which can be found at http://scala-ide.org/download/current.html. You don't need to to install Scala IDE explicitly, it is sufficient to just enable the respective update site. Eclipse will resolve the dependencies and pull only what is necessary to run KIV.


  • Java 1.7 or greater
  • Eclipse Kepler or Juno (older versions are currently untested)

Installation steps

  1. In Eclipse, select Help, Install New Software ...
  2. Add the update site for the Scala IDE for Scala for Scala version 2.11 (see here) and for KIV Eclipse https://swt.informatik.uni-augsburg.de/kiv/KIVEclipse
  3. From the KIV update site, install the features KIV Eclipse Integration and KIV Standard Library.
  4. After restarting Eclipse, you can open the KIV perspective under Window then Open Perspective -> Other.
  5. You may wish to read with the Quick Start

See also the Eclipse documentation: "Updating and installing software".

License Agreement

Copyright (c) 2013-present Department of Software Engineering, Augsburg University

KIV is copyrighted by University of Augsburg, Formal Methods group of the chair
of Software Engineering (Prof. Reif). This license grants the signer a
non-transferable and non-exclusive right to use KIV. This license is restricted
to noncommercial use. KIV is provided on an "as is" basis, without warranty or
liability of any kind. The Licensee agrees not to modify, or disassemble any of
the software files KIV consists of. This license is free of charge.

The KIV distribution contains two libraries: The Kodkod constraint solver and the JGraphX graph visualization package. During the installation you will be prompted to accept the respective licenses as well.


For general information and support please contact . For help with the installation, please contact .