Ziel des Projektes ist die Anwendung von am Institut für Symbolisches Rechnen der Johannes Kepler Universität Linz (RISC) entwickelten modernen Methoden der algorithmischen Logik und neuer algebraischer Techniken, auf konkrete Aspekte von Verfahren zuverlässiger Software-Verifikation, die von der Gruppe „Programmiersprachen und Compiler“ an der Eötvös Loránd Universität (ELTE) in Budapest entwickelt wurden.

Obwohl die Verifikation von Programmen und Algorithmen auf eine lange Forschungstradition zurückblickt, hat sie bislang nur geringe Bedeutung für die industrielle Software-Entwicklung (eine nennenswerte Ausnahme davon ist die Verwendung von Verifikationstechniken für den Test von Computer-Prozessoren). Es ist natürlich ein grundlegendes Ziel der Software-Industrie, den Entwurf und die Implementierung von Software zuverlässiger zu machen. Jedem Fortschritt in diesem Bereich kommt daher große Bedeutung für die Zukunft der IT-Branche zu.

Die in logischer Hinsicht komplexen und interessanten Teile des Software-Codes sind üblicherweise charakterisiert durch das Vorhandensein von (ineinander verschachtelten) Schleifen und Rekursionen. Gerade solche Code-Teile sind für die Anwendung von Methoden der formalen Verifikation geeignet. Formale Programm-Verifikation wird nur dann für die industrielle Anwendung attraktiv werden, wenn es gelingt einen ausreichend großen Anteil der Verifikationsarbeit zu automatisieren.

Arbeiten im Bereich der formalen Verifikation stimulieren das Studium neuer Formalismen der Logik als Temporallogik. Es ist sehr wichtig, die verschiedenen Beweismethoden, und die Verfahren der Computeralgebra und des automatischen Schließens, die am RISC für das automatische Beweisen von Theoremen und die deduktive Verifikation entwickelt wurden, miteinander in effizienter und effektiver Weise zu kombinieren, und sie auf eine Reihe konkreter, vom ELTE-Team zusammen­gestellter Anwendungsfälle anzuwenden. Ein geeigneter Anwendungsbereich wäre z.B. die Entwicklung von Komponenten verteilter, sicherheitskritischer Systeme.

Die beiden Forschungsgruppen, die Theorema-Gruppe (automatisches Schließen) des RISC und der Lehrstuhl „Programmiersprachen und Compiler“ an der ELTE, arbeiten an ähnlichen bzw. eng miteinander verwandten Problemen der Programm-Verifikation. Wir werden die Wirksamkeit der verschiedenen Ansätze der Gruppen vergleichen, indem praktische Probleme des Testens analysiert werden. Daraus kann abgeleitet werden, was die jeweils geeigneten Methoden sind, und notwendige Verbesserungen und Kombinationen der vorhandenen Methoden können vorgeschlagen werden.

• Automatisierte Generierung von Invarianten durch algebraische Methoden
• Automatisches Beweisen von Theoremen
• Verifikation von mobilem Code mithilfe algebraischer Methoden