Zum ersten Mal in der Geschichte der CADE ATP System Competition (CASC) hat ein einzelner automatisierter Theorembeweiser einen historischen Durchbruch erzielt: VAMPIRE gewann bei der 30. Ausgabe der CASC alle acht Wettbewerbskategorien – ein beispielloser Erfolg. Noch beeindruckender ist, dass VAMPIRE dabei mehr Probleme lösen konnte als alle anderen teilnehmenden Systeme zusammen. Dieser Triumph markiert einen Meilenstein für das Feld automated reasoning.
Der VAMPIRE-Theorembeweiser ist ein fortschrittliches Computerprogramm zur automatischen Beweisführung logischer Aussagen. Es verarbeitet gegebene Fakten und logische Regeln, um zu bestimmen, ob daraus neue Aussagen logisch folgen. Damit ist VAMPIRE besonders wertvoll in Bereichen wie der Softwareverifikation, Mathematik und Künstlichen Intelligenz, wo die Korrektheit und Nachvollziehbarkeit von Systemen von zentraler Bedeutung ist.
Doch nicht nur bei CASC konnte VAMPIRE überzeugen: Ein Fachbeitrag zur Entwicklung des Systems wurde zudem auf der renommierten International Conference on Computer Aided Verification (CAV) mit dem Distinguished Paper Award ausgezeichnet – einer der bedeutendsten Konferenzen für die Theorie und Praxis formaler Methoden in der Verifikation von Software- und Hardwaresystemen.
„Diese Erfolge sind nicht nur Einzelleistungen, sondern Ausdruck der gemeinsamen Stärke unserer Forschungsgruppe an der TU Wien Informatik, öffnet eine externe URL in einem neuen Fenster“, betont Laura Kovács, Leiterin des Instituts für Logic and Computation sowie des Forschungsbereichs Formal Methods in Systems Engineering. „Sie zeigen auch die enge Zusammenarbeit mit unseren Partner_innen an der University of Manchester, öffnet eine externe URL in einem neuen Fenster, der Tschechischen Technischen Universität, öffnet eine externe URL in einem neuen Fenster in Prag und der University of Southampton, öffnet eine externe URL in einem neuen Fenster. Das Ergebnis unterstreicht die führende Rolle der TU Wien in den formalen Methoden und die globale Relevanz unserer Forschung im Bereich automated reasoning.“
Der prämierte Beitrag, The VAMPIRE Diary, öffnet eine externe URL in einem neuen Fenster, wurde von Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdu, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl und Andrei Voronkov verfasst. Die Publikation dokumentiert die umfassenden Weiterentwicklungen, die VAMPIRE in den letzten zehn Jahren durchlaufen hat. Zu den jüngsten Fortschritten gehören unter andereem die Erweiterung auf komplexere Logiksysteme, die Einbindung leistungsstarker Techniken wie SAT/SMT-Solving und automatisierte Induktion sowie verbesserte Mechanismen zum Arbeiten mit unterschiedlichen Objekten, Regeln und Mustern.
„Es war eine lange, aber unglaublich spannende Reise – nicht nur hinsichtlich der technischen Entwicklung, sondern auch im Aufbau eines starken, engagierten Entwicklerteams“, resümiert Laura Kovács. „Die TU Wien ist in den letzten Jahren zu einem Zentrum der VAMPIRE-Entwicklung geworden. Besonders stolz bin ich aber auf unser motiviertes Team aus über 12 Expert_innen, das täglich daran arbeitet, VAMPIRE weiter zu verbessern und die Grenzen des automated reasoning zu verschieben. Diese Arbeit macht nicht nur Spaß, sie ist auch hochgradig inspirierend. Wir freuen uns über neue Mitwirkende!“
Herzlichen Glückwunsch an das gesamte Team zum beeindruckenden Erfolg bei CASC-30 und an alle Autor_innen des ausgezeichneten Papers!
Neugierig geworden? The VAMPIRE Diary ist als Open Access verfügbar und kann über Springer Nature, öffnet eine externe URL in einem neuen Fenster gelesen oder heruntergeladen werden.
Abstract zu The VAMPIRE Diary
In einem Jahrzehnt kontinuierlicher Weiterentwicklung ist VAMPIRE zu einem hochmodernen automatisierten Beweissystem für kombinierte Theorien gängiger Datenstrukturen gereift. Heute unterstützt VAMPIRE neben Arithmetik und Induktion auch höhere Logiken – eine Reaktion auf die wachsenden Anforderungen moderner Softwareverifikation. Dadurch ergänzt VAMPIRE nicht nur SAT- und SMT-Solver effektiv, sondern unterstützt auch interaktive Beweisassistenten. Der Beitrag erläutert praxisnahe Nutzungsszenarien von VAMPIRE und analysiert die zentralen Veränderungen seit der letzten Veröffentlichung, mit besonderem Fokus auf ingenieurstechnische Prinzipien und zentrale Designentscheidungen.