Computeralgebra und Theorembeweis für verifizierte Software

Das Ziel Formaler Verifikation ist es, eine Methodik bereitzustellen, mit der sicherere und robustere Systeme produziert werden können. Da die Komplexität von Software ständig zunimmt, gibt es ein wachsendes industrielles Interesse an der Anwendung formaler Methoden, um die Zuverlässigkeit langlebiger, hochwertiger Softwaresysteme, z.B. für Netzwerke, autonome Systeme und Verkehrskontrolle, zu gewährleisten. Die erfolgreiche Entwicklung und Anwendung leistungsfähiger Automated Reasoning Tools wie Modelchecker, statischer Analyseprogramme, Computeralgebra-Algorithmen, sowie Automatische Beweiser (Logik erster und höherer Ordnung) haben zu neuen Perspektiven und Herausforderungen für das Automatische Verifizieren geführt. Das Ziel des vorliegenden Projektes ist es, neue kombinierte Methoden von Computeralgebra und Theorembeweisen erster Ordnung zur statischen Analyse von Programmen, zu erschliessen. Diese sollen bestehende Methoden der Softwareverifikation übertreffen, die nicht über derartige fortgeschrittene algebraische Techniken und deren Kombination mit Theorembeweisern erster Ordnung verfügen. Wir werden dabei neue Theorien und Algorithmen für die automatische Synthese von Auxiliary Program Assertations entwickeln, die automatisch die Gültigkeit der Safety- und Liveness-Eigenschaften von Software prüfen können. Ein Haupthindernis beim Verifizieren derartiger Eigenschaften ist der Overhead, der durch die Erzeugung und Verifikation von Programm-Annotationen entsteht. Typische Assertions sind Schleifeninvarianten und Bedingungen an Ordnungsfunktionen. Die Komplexität bei der automatischen Erzeugung solcher Assertions hängt von Größe und Stuktur der Programme, der Programmiersprache, der Sprache der Assertions und der Logik des Theorembeweisers ab, sowie dessen Stärke, Art und Sprache. Verifikation ist generell unentscheidbar wenn unbeschränkte Datentypen, wie Felder, Listen, Pointers und uninterpretierte Funktionen verwendet werden. Darum konzentriert sich das Projekt auf die Entwicklung von Methoden, die effizient komplexe Programmstrukturen und unbeschränkte Datentypen bewältigen können. Dabei werden automatisch Programm-Annotations generiert, die zum Prüfen der Korrektheit von Programmen eingesetzt werden. Speziell wollen wir Techniken des Symbolischen Rechnens anwenden, die im Gegensatz zu existierenden Methoden automatisch polynomielle Invarianten und Ordnungsfunktionen finden und durch eine Kombination von Automatischem Beweisen mit Computeralgebra im Gegensatz zu derzeitigen Werkzeugen auch quantifizierte Invarianten mit alternierenden Quantoren ableiten können. Diese Methoden sollen weiters die Erzeugung von Verifikationsbedingungen mit der automatischen Erzeugung von Schleifeninvarianten und Ordnungsfunktionen kombinieren und die Leistungsfähigkeit aktueller Theorembeweiser nutzen und ergänzen. Um diese Ziele zu erreichen, wird die Forschung in vier Schwerpunkte eingeteilt. (1) Synthese von Assertions, (2) automatische Programmverifikation, (3) Beweisen von Programmeigenschaften, und (4) Entwicklung und Evaluierung von Softwaretools. Unser Forschungsprojekt zielt insbesondere auf eine Klasse von imperativen (sequentiellen) Schleifen ab, und beschäftigt sich mit der Entwicklung neuer Theorien, Technologien und Werkzeuge für die automatische Verifikation solcher Programme.