The KIV System
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.
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
- September 2024: New Visual Studio Code extension: download and installation.
- April 2023 KIV v10: Several bugfixes and improvements. Note that the file format has changed and old projects can not be used with KIV v10. If you need to convert an old project, send an email to Gerhard Schellhorn.
- July 2022 New overview paper of the KIV system: Software & System Verification with KIV.
- April 2022 Updated version of the KIV plugin, compatible with the latest versions of the Eclipse IDE.
- May 2021 Participation at the VerifyThis Verification Competition (Best Student Team), and solutions.
- May 2019 Participation at the VerifyThis Verification Competition, and solutions.
- October 2018 KIV v9: Several bugfixes and improvements. Note that the file format has changed and old projects can not be used with KIV v9. If you need to convert an old project, send an email to Gerhard Schellhorn.
- November 2017 Participation at the VerifyThis Verification Competition (Best Student Team), and solutions.
Installation in Eclipse
KIV comes as an Eclipse plugin which you can download from the update site listed below.
?
Installation steps
- Download and install the Eclipse IDE for Java Developers via the Eclipse download site ( https://www.eclipse.org/downloads/packages/release/2022-03/r). Currently, it is recommended to use version 2022-03 (4.23), newer versions could occasionally cause problems. In case you run into problems with version 2022-03 (4.23) as well, the Oxygen version can still be used ( https://www.eclipse.org/downloads/packages/release/oxygen/3a).
- In Eclipse, select Help?→ Install New Software ....
- Add the update site for KIV for Eclipse? https://kiv.isse.de/releases/v10/stable/site and install the features KIV Eclipse Integration and KIV Standard Library as well as all necessary KIV Dependencies.
- After restarting Eclipse, you can open the KIV perspective under Window then Open Perspective?→ Other.
- 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 or newer (the plugin is developed with ScalaIDE, which is based on Eclipse Oxygen, so other Eclipse versions are currently not tested exhaustively)
?
License Agreement
Copyright (c) 2013-present Department of Software Engineering, Augsburg 新万博体育下载_万博体育app【投注官网】 KIV is copyrighted by 新万博体育下载_万博体育app【投注官网】 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.
Installation in Visual Studio Code
KIV is now also available as a Visual Studio Code extension. However, it does not contain all features yet.
?
Installation steps
- Download and install the latest version of Visual Studio Code from https://code.visualstudio.com/.
- Get the latest version of the KIV extension?"kiv-editor-x.y.z.vsix" and the KIV Library extension "kiv-library-x.y.z.vsix" from https://kiv.isse.de/releases/v10/vscode/latest/.
- In Visual Studio Code, navigate to the ?Extensions“ view.
- Select ?Views and More Actions...“ → ?Install from VSIX...“ and select the downloaded archive of the KIV extension (installation may take a few moments).
- Repeat this step for the KIV Library extension.
- After installation, a new "KIV" view should be added to the navigation bar.
- To activate KIV syntax highlighting, a KIV color theme must be activated. Navigate to ?File“ → ?Preferences“ → ?Theme“ → ?Color Theme“ and select one of the KIV themes ("KIV Light" or "KIV Dark").
Requirements
- Java 21 (or greater)
- Visual Studio Code
License Agreement
Copyright (c) 2013-present Department of Software Engineering, Augsburg 新万博体育下载_万博体育app【投注官网】 KIV is copyrighted by 新万博体育下载_万博体育app【投注官网】 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.
?
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 新万博体育下载_万博体育app【投注官网】 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.