IMPROVE APS

The vision for this project is to advance technology such that regression verification methods are available that will be routinely used for ensuring correctness in the evolution processes for long-living reliable systems requiring frequent re-validation. The goal of regression verification is to formally prove that software remains correct through its evolution, changes have the desired effect, and no new bugs are introduced. Regression verification avoids the main bottleneck for the routine practical use of formal verification, namely the need to write full functional specifications (which is a huge effort). Also, given two program versions or variants that are both complex but similar to each other, the effort for verifying the relation between them mainly depends on the difference between the programs and not on their overall size and complexity. IMPROVE-APS Project

KASTEL

The main topics intelligent infrastructure, cloud computing and public security challenge the IT security of the future. In addition to the classical term of security one has to deal with threats from the inside as well. It is not enough anymore only to look at security issues of system components. We have to focus on transdisciplinary methods. The Kompetenzzentrum für Angewandte Sicherheits-TEchnoLogie (KASTEL) is a research center for cyber security and combine several areas of IT security and their users.

KeY

The KeY System is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly as possible. At the core of the system is a novel theorem prover for the first-order Dynamic Logic for Java with a user-friendly graphical interface. The project was started in November 1998 at the University of Karlsruhe. It is now a joint project of KIT, Chalmers University of Technology, Gothenburg, and TU Darmstadt. The KeY tool is available for download.

DeduSec: Program-level Specification and Deductive Verification of Security Properties

In recent years tremendous progress has been achieved in formal verification of functional properties of computer programs. At the same time seminal papers have been published showing that it is in principle possible to formulate information-flow problems as proof obligations in program logics. The overall goal of the project is to leverage these advances together with our own experience in formal methods for functional properties in order to specify and verify security properties. DeduSec Project

xorblast

A CNF preprocessor for xor constraints with support of Gauss-Jordan elimination.

#PI

... soon ...

ReVeForPLC

iec61131lang Parser and AST for languages of the IEC61131 norm.

Medical Simuation Markup Language (MSML)

msml at Github.
The medical simulation markup language (MSML) is a flexible XML-based description for the biomechanical modeling workflow and finite-element based biomechanical models. MSML helps you to create biomechanical models from tomographic data, export them to FE solvers and analyze the results. It is very flexible as already existing components (e.g. segmentation algorithms, meshers) can usually be integrated into the framework by providing a single additional XML-file. MSML was created in the SFB125 in a coorperation between KIT and DKFZ.