© University of Augsburg

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

  1. 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,
  2. for semantical foundations of programming languages from a specification of the semantics down to a verified compiler,
  3. for building security models and architectural models as they are needed for high level ITSEC or CC evaluations.

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 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 uses the Scala programming language and is integrated into the Eclipse platform as a plugin.

News

Installation

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.12, which can be found at http://scala-ide.org/download/sdk.html. You should install the Scala IDE, which already has the Scala plugin. Eclipse will resolve the dependencies and pull only what is necessary to run KIV. Note that previous versions of Scala are incompatible.

 

Installation steps

  1. In ScalaIDE, select Help → Install New Software ....
  2. Add the update site for KIV for Eclipse https://swt.informatik.uni-augsburg.de/kiv/v9/stable/site and install the features KIV Eclipse Integration and KIV Standard Library as well as all necessary KIV Dependencies.
  3. After restarting Eclipse, you can open the KIV perspective under Window then Open Perspective → Other.
  4. You may wish to read the Quick Start.

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

 

Requirements

  • Java 1.8 or greater
  • Eclipse Oxygen (older versions are currently untested)

 

Previous Eclipse Update Sites

 

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.

Institute for Software & Systems Engineering

The Institute for Software & Systems Engineering (ISSE), directed by Prof. Dr. Wolfgang Reif, is a scientific institution within the Faculty of Applied Computer Science of the University of Augsburg. In research, the institute supports both fundamental and application-oriented research in all areas of software and systems engineering. In teaching, the institute facilitates the further development of the faculty's and university's relevant course offerings.

Search