KIV Projects for the Ph.D. Thesis of Holger Grandy

Here are all formal proofs for the Ph.D. thesis

"Formale Verifikation der Korrektheit sicherheitskritischer Java Anwendungen" (in german)

by Holger Grandy . All proofs were done with the KIV system. The project pages linked from here can be viewed with most modern web browsers. Best view is provided when using Firefox 2.0, Internet Explorer may have some problems displaying unicode characters for logical symbols.

Transformation and Check Layer / Generic Infrastructure Library

The transformation layer of chapter 10 in the thesis is implemented and verified in the following KIV project: ASN1-light: A Verified Message Encoding for security protocols

You also find the whole document library (e.g. functions java2doc, doc2java, validDoc, ...) in this project.

Cindy

The Cindy Case study consists of two projects:

Mondex

The Mondex Case study consists of multiple projects. A complete list of all KIV projects for the Mondex case study can be found on this site .

The reference implementations for the case study can be found here .

The main development for the thesis is the correctness proof for one of the implementations. View the Java refinement project

Libraries



[Impressum] [E-Mail]