Certifying Algorithms for Interactive Components and Distributed Systems

A certifying algorithm produces not only a result, but also a witness, who shows the result's correctness. In the best case, the witness is self-explanatory. Otherwise, a (comparatively simple) checker algorithm verifies the witness. Since the 2000s, certifying variants of numerous "classic" algorithms have been developed. Modern computer-integrated systems and infrastructures are often built from interactive components, forming a distributed system of loosely coupled and interactive nodes. Algorithms for interactive components generally do not terminate. Furthermore, the components of a distributed system usually do not know the layout of the entire system structure. Therefore, algorithms for such components and systems behave fundamentally differently than classic algorithms. This project researches, to what extend the concept of certification can be applied to interactive components and distributed systems. This question is particularly interesting because interactive components and distributed systems are much harder to implement than classical algorithms. Furthermore, their formal verification is still beyond the state of the art.

Principal Investigators
Reisig, Wolfgang Prof. Dr. rer. nat. habil. (Details) (Software Engineering and Theory of Programming I)

Duration of Project
Start date: 01/2015
End date: 07/2019

Last updated on 2021-14-01 at 15:29