Gurevichs "Abstract State Machines" (ASM) sind ein Modellierungsformalismus mit dem Anspruch, den Zusammenhang eines realen oder geplanten Systems mit einem formalen Modell besonders natürlich, eng und nahtlos gestalten und formulieren zu können. Dies gelingt mit der Idee, Zustände als mathematische Strukturen aufzufassen, deren syntaktische Darstellung unerheblich ist. Wie in der Mathematik üblich, argumentiert man über einzelne Aspekte einer solchen Struktur mit Hilfe von Termen über einer Signatur S. Mit solchen Termen werden zudem Programme (im elementaren Fall konventionelle parallele bedingte Wertzuweisungen) formuliert, die dynamisches Verhalten, also Schritte, als Paare von Zuständen beschreiben. Die Forschung des Lehrstuhls konzentriert sich auf Fragen der Ausdruckskraft von ASM, ihren Bezug zu anderen Systemmodellen und ihre Verwendung zur Modellierung von Web Services, insbesondere die Sprache BPEL4WS.