Eine formale Semantik besteht aus einem mathematischen Modell für eine Programmier- oder Systembeschreibungssprache. Sie dient dazu, gewisse Beziehungen zwischen Programmen/Systemen und/oder ihren Spezifikationen zu beweisen. Dies betrifft zum einen die Verifikation eines Systems relativ zu einer gegebenen Spezifikation, zum anderen die Transformation, d. h. verfeinernde Umformung von Spezifikationen in ausführbare Systeme oder von Systemen in effizientere Formen. Ziel moderner algebraischer Ansätze hierzu ist es, sowohl die in der semantischen Beschreibung involvierten Ausdrücke wie auch den zugehörigen Beweiskalkül möglichst knapp und durchsichtig zu machen, indem Logik soweit wie möglich in Algebra kompaktifiziert wird. Neben den mathematischen Grundlagen werden in der Vorlesung einige wichtige semantische Konzepte sequentieller und paralleler Systeme und die wesentlichsten Transformationstechniken besprochen. Anwendungsbeispiele stammen aus dem Software– und Hardware-Bereich.
