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

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

VerifAPS — Verification for Automated Production System

• iec61131lang Parser and AST for languages of the IEC61131 norm.
• iec61131lang Symbolic Execution and Code Transformation for Sequential Function Charts and Structured Text.
• iec-xml Support of PCLOpenXML.
• smv-model AST and Generation of SMV modules.
• geteta (GITHUB) Verification Engine for Generalized Test Tables

#PI — QIF analysis for C

#PI is a tool for analysis of Quantified Information Flow for C programs.

xorblast

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

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.