Formale Methoden dienen der Erstellung nachweisbar korrekter Systeme, sowohl in Soft- wie in Hardware. Hierzu gibt es zwei wesentliche Ansätze:

• Umformung einer (häufig noch nicht ausführbaren) formalen Spezifikation durch Semantik-treue Transformationen in eine per Konstruktion korrekte Implementierung (Transformations-/Verfeinerungsansansatz)
• Angabe von Spezifikation und Implementierung mit anschließendem Beweis der Korrektheit der Implementierung relativ zur Spezifikation (Verifikationsansatz).

Beide dieser Ansätze, insbesondere aber der Transformationsansatz, können für auch nur halbwegs realistische Systeme nur dann in voller Formalität durchgeführt werden, wenn in großem Umfang algebraische Techniken eingesetzt werden, die viele kleine logische Umformungsschritte durch Anwendung eines einzigen großen (Un-)gleichungsschritts ersetzen. Hierzu sind geeignete algebraische Strukturen und Modellierungsmöglichkeiten zu finden.

Als grundlegende algebraische Strukturen zur Systembeschreibung haben sich unter anderem Halbringe, Kleene-Algebren und Omega-Algebren erwiesen. Die gegenwärtigen Forschungsarbeiten der Professur beschäftigen sich mit der Weiterentwicklung und Anpassung dieser Strukturen in konkreten Anwendungsfällen.

Unabdingbare Grundlage für die formale Systembeschreibung und -entwicklung ist eine formal definierte Semantik für die Konstrukte der verwendeten Spezifikations- und Implementierungssprachen. Um einen nahtlosen Übergang zu ermöglichen, werden auch hier algebraische Techniken zur Semantikdefinition eingesetzt, so dass die zugehörigen Gesetze direkt für die Systementwicklung nutzbar werden.