Running Projects

• 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

• Organic Computing

  Systematic design of reliable Organic Computing applications.

• SoftRobot

  The development of a new software architecture for industrial robots.

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.

Finished Projects

• 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