Bisherige Korrektheitsuntersuchungen zu verteilten Systemen basieren oftmals auf lediglich informellen oder semi-formalen Methoden. Unsere Vision ist es, systematisch Techniken der formalen Semantik und mathematischen Logik, wie sie im Gebiet der Concurrency Theory seit etwa 30 Jahren entwickelt werden, anzuwenden und anwendungsorientiert weiter zu entwickeln. Schließlich soll die Korrektheit verteilter Systeme nicht nur mit Bleistift und Papier, sondern durch rechnergestützte Beweiswerkzeuge automatisch überprüfbar bewiesen werden. 

Schon heute zeichnet sich ab, daß sich Theorien für verteilte Systeme nicht auf den Bereich verteilter Rechnersysteme beschränken müssen. Konkrete Anwendungen in so unterschiedlichen Bereichen wie der Geschäftsprozessmodellierung und der Systembiologie stellen hier überaus vielversprechende Einsatzgebiete für unsere Grundlagenarbeit dar.