Projekt S1 entwickelt Algorithmen für die kompositionale Verifikation komplexer verteilter Systeme. Die Algorithmen analysieren partielle Designs, in denen Teile des Systems als "Black Boxes" ausgeblendet sind, und leiten aus Eigenschaften der partiellen Designs Eigenschaften des Gesamtsystems ab. Das zentrale Ziel des Projekts ist die Steigerung der Skalierbarkeit und der Präzision der Analyse mit Hilfe von Algorithmen und Heuristiken für das Lösen unendlicher Spiele, einschliesslich gezeiteter Spiele und Spiele mit unvollständiger Information, QBF-Lösungsverfahren und Methoden zur automatischen Abstraktionsverfeinerung. Neue Themen der dritten Förderperiode sind die Analyse parametrierter Systeme und die Synthese von Korrektheitszertifikaten.