Selected KIV Projects

For some of the projects done with the KIV system we provide XML representations of the specifications, theorems and proofs. The project pages can be viewed with most modern web browsers. All xml files in these projects are generated automatically, but not at the same time. Since projects may depend on other projects, the following situation can occur: A theorem in project A uses a theorem from project B, but the link to this theorem is dead. This does not mean that the project is inconsistent, but simply that the documentation is not up-to-date.

Verification Competitions

Verification competitions aim at testing tool-usability and the ability of human proof engineers to quickly solve correctness assertions and to find invariants for different small, but often tricky problems. Some of the competitions we have participated in are:


The Verified Flash File System

Project Flashix deals with the development of a fully verified flash file system. Some KIV projects are:


Software Transactional Memory (STM)

Concurrency and Linearizability

Project VeriCAS deals with the development and application of formal methods for the verification of concurrent algorithms. We are tracking two main approaches. Our first approach is based on pure HOL and the Owicki-Gries Method. Some KIV projects are:

Our second approach is based on the logic RGITL, which is based on Interval Temporal Logic (ITL) and Rely-Guarantee (RG) Reasoning:

Security

Project SecureMDD deals with techniques that facilitate the development of security-critical applications that are based on cryptographic protocols. Here are some KIV projects:

Project IFLow integrates formally verified information flow control (IFC) properties and language based type systems for IFC with a software engineering approach based on model driven development.


General Java Verification

Abstract State Machines
General Refinement Theory

The KIV Library

Here is a list of further (completed) projects.



[Imprint] [Data Privacy Statement] [E-Mail]