The institute is actively working on new techniques for formal system development. Our research focuses on refinement as a method of modular, step-wise, top-down development of a system starting with an abstract formal specification. The methodology for sequential systems is based on Abstract State Machines. Concurrent system analysis relies on the compositional temporal program logic "RGITL". Our group develops and distributes the KIV system, an interactive theorem prover that supports these techniques. We are currently working on the Flashix project, which aims at the development of a verified file system for flash memory.

Senior Researcher
Institute for Software & Systems Engineering
  • Phone: +49 821 598 2124
  • Email:
  • Room 3016 (Building N)

Hot Topics

Refinement

Modular, step-wise, top-down development of a system starting with an abstract formal specification

Temporal Logic

Concurrent system analysis relying on the compositional temporal program logic "RGITL"

Interactive Theorem Proving

Development and application of interactive theorem proving tools and techniques

 

The goal of formal methods in software engineering is to provide techniques for developing highly reliable as well as security critical software. Two steps are required to achieve this goal: An unambiguous specification of the system requirements and a mathematical proof (verification) that the implementation adheres to this specification.
Formal methods provide a wide variety of mathematically precise specification languages, such as higher order logic, algebraic specifications, abstract state machines, the Z notation, and temporal logic. These languages enable the unambiguous description of a system's expected behavior, thereby forming the basis of the later verification of the system's correctness. System correctness consists of different aspects ranging from functional correctness over safety and security to reliability.
Mathematical proofs of system correctness can be constructed using several approaches, such as interactive theorem proving, static code analysis, model checking, and SMT solving.
An important concept to handle complexity is refinement, which allows a modular, step-wise, top-down development of a system starting with an abstract formal specification, ending with verified code.
We are actively working on new techniques for formal system development. Our research focuses on refinement in combination with abstract state machines and temporal logic. Our group is developing the KIV System, an interactive theorem prover. We apply these techniques in practical applications, such as in our research projects VeriCAS (correctness of lock-free algorithms) and Flashix (development of a verified file system for flash memory).
We are offering our students lectures, lab courses, and seminars on formal methods and their application in the software engineering process.

Tools & Projects

KIV System

A Tool for Formal Systems Development and Interactive Verification

KIV Logo

VeriCode

Correct Translation of Abstract Specifications to C-Code

Flashix

Construction and Verification of a State-of-the-Art File System for Flash Memory

Flashix Logo

Services

  1. Proving the functional correctness of safety- and security-critical systems

  2. Consulting/training in the use of formal methods for the certification of software that meets the highest safety and security standards (e.g., SIL, Common Criteria)

Completed Projects

VeriCAS

Verification of Lock-Free Concurrent Algorithms

Go!Card

Formal Methods for Secure Java Smart Cards

FORMOSA

Integrating Formal Models and Safety Analysis

InopSys

Interoperability of Calculi for System Modelling

Protocure

Ensuring Quality in Healthcare

Team

Director
Institute for Software & Systems Engineering

Homepage:

Email:

Senior Researcher
Institute for Software & Systems Engineering

Homepage:

Email:

Institute for Software & Systems Engineering

The Institute for Software & Systems Engineering (ISSE), directed by Prof. Dr. Wolfgang Reif, is a scientific institution within the Faculty of Applied Computer Science of the University of Augsburg. In research, the institute supports both fundamental and application-oriented research in all areas of software and systems engineering. In teaching, the institute facilitates the further development of the faculty's and university's relevant course offerings.

Search