• Completed Projects

Running Projects

• IFlow

  IFlow: Developing Systems with Secure Information Flow.

• SecureMDD

  SecureMDD: Model Driven Development of Secure Systems.

• SAVE ORCA

  Systematic design of reliable Organic Computing applications.

• OC-Trust

  Trustworthy Organic Computing systems.

• SoftRobot

  The development of a new software architecture for industrial robots.

• VeriCAS

  Verification of Lock-Free Concurrent Algorithms.

• Flashix

  Verification of a File System for Flash Memory.  

 

KIV projects on the WWW

A browsable representation of the formal specifications as well as the theorem bases and the proofs of some of our recent case studies, which were verified with the KIV system, can be found on our KIV projects page.

Completed Projects

• CFK-Tex

  Automated handling and draping of limp carbon fibre fabrics.

• INOPSYS

  Interoperable combination of logics and specification formalisms, in particular temporal logic, state charts, reasoning about communication streams.

• Protocure

  Specification and Analysis of Health-Care protocols

• Go!Card

  Development of a framework for E-Commerce applications: abstract specification and verification security protocols, refinement down to Java code, use of Java Smartcards.

• ForMoSA

  Safety Analysis in combination with formal methods applied to embedded systems.
• DFG Research Programme "Deduction"
• Digital Signatures
• SMaCOS
• Verification Support Environment (VSE)
• VSE II