Das Projekt R1 erforscht die automatische Verifikation von Realzeitsystemen, die durch Spezifikationen mit den drei Dimensionen Prozessverhalten, komplexen unendlichen Datenstrukturen und kontinuierlicher Zeit beschrieben werden. Dazu werden Transformations- und Dekompositionstechniken mit Beweisverfahren verknüpft, die auf den Paradigmen der Abstraktionsverfeinerung und der lokalen Theorieerweiterung beruhen.