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. Best view is provided when using Firefox 3.x. 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:

COST Verification Competition 2011 (Web presentation of our solutions)
VSTTE Verification Competition 2011 (Web presentation of our solutions)

The Verified Flash File System

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

Specification of B+trees that are verified with the help of shape analysis
Abstract Specification of the UBIFS File System for Flash Memory (Web Presentation for FM 09 paper)

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:

Linearizability proofs for a lock-free stack (Web Presentation for FMOODS 2008 paper)
Linearizability proofs for a lock-free stack and an implementation of sets using fine-grained locking (Web Presentation for journal version of FMOODs 08 paper)
Verification of Linearizability as Refinement using Possibilities (Web Presentation for FM 2011 paper)
Verification of Linearizability of Herlihy and Wing's queue example (Web Presentation for a submitted paper; based on the previous theory)

Our second approach is based on Temporal Logic and Rely-Guarantee Reasoning. More details can be found here:

Temporal Logic Specification and Verification of Concurrent Algorithms

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:

The Mondex Challenge
Yet another version of the copy card
The Electronic Wallet (E-WALLET) Case Study
E-Wallet Extended (The electronic wallet with an arbitrary number of cardlets and terminals)

PROSECCO-lib (The basic library for modeling Smart Card applications in PROSECCO)
E-Wallet-V2 (The specification of the E-Wallet case study based on PROSECCO-lib)
CINDY case study (Cinema tickets on your mobile)
CINDY-ref (Refinement to a Java program)
An algebraic theory of messages (Used in the verification of cryptographic protocols)

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

The Java Verification project
Formal Java Semantics
ASN1-light (A Verified Message Encoding for security protocols)
Generic Java documents (Used in the CINDY case study above, to represent abstract documents for message exchange in Java)

General Refinement Theory

A formalisation of relational concurrent refinement (This is a version of data refinement where data types have external and internal operations. Operations may be blocked and sets of blocked operations are used as final observations (refusals). The possibility of an infinite run of internal operations is interpreted as divergence. This allows to prove that data refinement for such data types coincides with failures-divergence refinement in CSP. More information is given in the paper on which this case study is based.)
Completeness proofs for ASM Refinement and for IO Automata refinement (Web Presentation for ENTCS Special Issue at FM 08)
Completeness proofs for Fair ASM Refinement (Web Presentation for FAC Special Issue at FM 08)

The KIV Library

The basic KIV library (Basic data type specifications)
Extensions to the KIV library (Additional data type specifications)

Here is a list of further (completed) projects.