LoLA gewinnt Gold (1. Platz) in den Kategorien „UpperBounds“ und „LTL Formulas“ sowie Silber (2. Platz) in den Kategorien „Reachability Formulas“ und „CTL Formulas“. Weiterhin gewinnt LoLA die erstmals vergebenen Sonderpreise für die schnellste Laufzeit in den Kategorien „UpperBounds“, „Reachability Formulas“ und „LTL Formulas“ sowie für den sparsamsten Speicherplatz in den Kategorien „UpperBounds“ und „LTL Formulas“.
Im Wettbewerb mussten zu fast 1.000 Systemmodellen insgesamt mehr als 104.000 Anfragen zum Systemverhalten beantwortet werden. Der Wettbewerb stellt einen wichtigen Anreiz zur Weiterentwicklung von Analysewerkzeugen dar. Darüber hinaus erlaubt der Wettbewerb einen Vergleich der Ergebnisse zwischen den Teilnehmern. Dadurch konnte in den letzten Jahren die Verlässlichkeit aller teilnehmenden Werkzeuge erheblich gesteigert werden. Der Lehrstuhl unterstützt den Wettbewerb darüber hinaus durch die Bereitstellung von umfangreichen Rechnerkapazitäten.
LoLA ist ein Petri-Netz-Verifikationswerkzeug. Seine Entwicklung begann im Jahr 1998 durch den jetzigen Inhaber des Lehrstuhls für Theoretische Informatik Prof. Dr. rer. nat. habil. Karsten Wolf und wird als Projekt des Lehrstuhls sowie durch eine Reihe von Projektveranstaltungen auch durch Studierende weiterentwickelt. Es bietet zahlreiche Methoden an, um mittels Analyse der Systemstruktur und der Exploration eines möglichst kleinen Teils des Zustandsraumes Anfragen über das Verhalten eines als Petrinetz modellierten Systems zu beantworten. LoLA war und ist Gegenstand zahlreicher wissenschaftlicher Arbeiten, Publikationen und mehrerer Drittmittelprojekte. Es wird vom Lehrstuhl der internationalen Wissenschaftscommunity zum freien Download zur Verfügung gestellt. LoLA wurde bereits in mehrere andere Tools erfolgreich integriert und konnte bei der Bearbeitung von Real-Life-Fragestellungen in mehreren Anwendungsgebieten helfen.
Der Model Checking Contest @ Petri Nets (MCC) ist der internationale Wettbewerb zur Bewertung von Werkzeugen für die formale Verifikation von verteilten Systemen, die auf Petrinetzen basieren. Durch den Vergleich der Werkzeuge sollen besonders geeignete Techniken identifiziert werden, mit denen bestimmte Arten von Problemen erfolgreich bearbeitet werden können, z.B. Zustandsraumerzeugung, Deadlock-Erkennung, Erreichbarkeitsanalyse, Kausalanalyse. Der Wettbewerb besteht aus zwei Phasen: dem „Call for Models“ und dem „Call for Tools“. Beim „Call for Models“ werden Petrinetz-Modelle aus der Fachcommunity vorgeschlagen und zusammengetragen; beim „Call for Tools“ werden Werkzeuge eingereicht und dann Leistungstests an den zusammengetragenen Modellen unterzogen. Der Wettbewerb wird seit dem Jahr 2011 jährlich im Rahmen der International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS) ausgetragen, die seit 1980 ebenfalls jährlich an wechselnden Orten weltweit stattfindet.