Current Projects

The research topics of our group include formal, logic-based methods for the specification, verification and analysis of software. The main goal is to increase the reliability and security of critical systems.

Besides methods for the verification of functional correctness of software, our group develops methods for proving information-flow properties, especially for IT-security applications. The considered scenarios include a variety of applications such as object-oriented software, software for industrial factory automation and e-voting systems.


COST Action IC1205: COMSOC

Computational Social Choice

Computational social choice is a rapidly evolving research trend concerned with the design and analysis of methods for collective decision making. It combines methods from computer science with insights from economic theory. COST Action IC1205 on Computational Social Choice is a European research network that has been set up to provide a common platform for research in this field across Europe and beyond.

Within this project, we focus on the specification and verification of voting schemes (a.k.a. voting rules). A voting scheme, as a method to combine individual preferences to an aggregated election result, is part of the fundamental democratic principles. It is thus vital that voting schemes are working as intended. The goal of this project is to develop formal verification techniques which allow to check properties of voting schemes without the huge overhead of user interaction needed in full functional verification. The resulting methodology could then be used in an iterative design and implementation process of new voting schemes.

COST Action

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

Software Campus Project: FIfAKS

Formal Information-Flow Analysis of Component-Based Systems

Goal of the Software Campus programme is the training of tommorow's managers with excellent IT background. Projects in the scope of the Software Campus programme are supported by scientific and industrial partners.

The project "Formal Information-Flow Analysis of Component-Based Systems" is a project in collaboration with DHL IT-Services in Bonn and aims at performing security analysis of component-based systems during system design.

FIfAKS Project

IMPROVE APS

Regression Verification in a User-Centered Software Development Process for Evolving Automated Production Systems

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

KASTEL Project

KeY

Integrated Deductive Software Design

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

KeY Project

Lehre hoch Forschung-PLUS

Problem-oriented, Research-oriented and Interdisciplinary Teaching in Computer Science

The main goal of the project LehreForschung-PLUS is to improve the study conditions and to continuously raise the qualitiy of teaching by an extensive development of the curricula for bachelor and master students.

Our subproject comprises three primary actions, which all aim to implement and strengthen project- and research-oriented, as well as interdisciplinary, teaching in the computer science curricula.

These comprise the further development and improvement of the project- and research-oriented master module "Research Practice", the project-oriented bachelor module "Software Engineering Practice", as well as the introduction of the interdisciplinary and research-oriented master profile "Internet and Society".

Subproject "LehreForschung-PLUS – Problem-oriented, Research-oriented and Interdisciplinary Teaching in Computer Science"


Finished Projects

COST Action IC0701: Formal Verification of Object-Oriented Software

The main objective of the Action is to develop verification technology with the reach and power to assure dependability of object-oriented programs on industrial scale.

COST is the acronym for "European Cooperation in the Field of Scientific and Technical Research".  It is an inter-governmental framework for fostering collaboration between researchers in Europe in a "bottom-up" manner. More information about COST can be found at the official COST website. COST is organized in Actions. The goal of this Action is to co-ordinate the development of verification technology, to achieve reach and power needed to assure reliability of object-oriented programs on industrial scale.

COST Action

GIF: Reliable Software Evolution

In diesem Projekt werden Testverfahren und formale Methoden kombiniert um die Zuverlässigkeit von evolvierender Software zu gewährleisten. Mit dem Fokus auf evolvierende Software behandeln wir eine wichtige Phase im Lebenszyklus eines Softwaresystems und heben die inkrementelle Natur von Softwareänderungen hervor.

GIF Project

IMPROVE

Regression Verification for Evolving Object-Oriented Software

The goal of this project is to leverage advances in deductive program verification to enable regression verification, i.e., proving formally that software remains correct through its evolution, and no new bugs are introduced. We aim to develop a regression verification methodology for a real object-oriented language (Java) that has the reach and power to be applied to real-world software

IMPROVE Project

Integration of Deduction-Based Verification and Model Checking for Machine-Oriented Software

The integration of deductive software verification and bounded model checking (BMC) is subject of our current activities and is joint work together with the working group of Dr. C. Sinz.

Proving software correct using deductive verification methods needs — in addition to the requirement specification — a variety of interactions by the user of the tool (e.g., giving loop invariants or specification of auxiliary functions). In contrast, BMC to a large extent doesn't rely on user support in proofs. On the other hand, deductive program verification features a higher precision and a more expressive specification language compared to BMC.

A first goal of the work in this project to combine the strengths of both methods is to use BMC to improve interaction of the user with the deductive verification tool. By linking a BMC-tool to a deductive verification framework, parts of the specification of a program can already be checked even before starting with the whole deductive proof.

Lehre hoch Forschung

Problem-oriented Teaching

The main goal of the project "Lehre hoch Forschung" is enhancing study conditions and teaching quality as well as the integration of research topics into early stages of the study programme for bachelor and master students.

Moreover, “Lehre hoch Forschung” is aimed at offering a wide scope of prospective problem-oriented and research-oriented practical courses and projects to students already during their early semesters. The students gain insights into aspects relevant to fundamental and applied research, as well as inter- and trans-disciplinary competences.

Our group is responsible for the establishment and coordination of the master course module "Research Practice". This is a project-oriented course in which students learn how to do research projects: from the early stages of writing a project proposal to performing the project tasks and writing publications. The projects are performed on topics within current research projects.

Subproject "Lehre hoch Forschung – Problem-oriented Teaching"

Software Campus Project: USV

Usability of Software Verification Systems: Evaluation and Improvement

Goal of the Software Campus programme is the training of tommorow's managers with excellent IT background. Projects in the scope of the Software Campus programme are supported by scientific and industrial partners.

The project "Usability of Software Verification Systems: Evaluation and Improvement (USV)" is a project in collaboration with DATEV eG in Nürnberg and aims at evaluating the usability of software verification systems. Based on the evaluation results mechanisms will be developed to improve the productivity of such systems.

USV Project

Verisoft XT

The main goal of this project is the pervasive formal verification of computer systems

The correct functionality of systems, as used in e.g. automotive or in the area of safety engineering, is checked using formal, mathematical methods.

Scenarios

  • automotive applications
  • avionic applications
  • operating systems and hypervisors

Formal correctness proof of an embedded operating system kernel

The main focus of the investigations of our research group is on the specification and verification of a microkernel with partitioning features which is used in industrial avionic applications. For this we employ the verification tool VCC developed by Microsoft Research,  to formally verify functional properties of the implementation of the microkernel PikeOS from SYSGO AG.

Verisoft Project