Skalierbare saturation-basierte Verfahren für die Verifikation von Programmen höherer Ordnung

• Antragsteller: Dr. Christopher Broadbent; Professor Dr. Javier Esparza
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2013 bis 2016
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 232350543

Das funktionale Programmierparadigma, Grundlage von Sprachen wieFsharp, Scala, Haskell, und OCaML, gewinnt zunehmend an Bedeutung. Größere und komplexere Anwendungen im Finanz- und Web-bereich führen zu wachsendem Interesse an Verfahren und Werzeuge zur Analyse und Verifikation funktionaler Programmen. Die grösste Herausforderung bei der Entwicklung dieser Verfahren sind Analysemethoden für Funktionen höherer Ordung. Aus diesem Grund ist in den letzten Jahren Higher-Order Model Checking sehr intensiv untersucht worden. Insbesondere wurde neulich ein automaten-theoretischer Ansatz auf der Basis con Collapsible Pushdown Automata (CPDA) entdeckt. Die Ziele des Projekts sind die Entwicklung von Model-Checking-Algorithmen zur automatischen Verifikation von Sicherheitseigenschaften von Programmen höherer Ordung modelliert als CPDA und deren Implementierung als Softwareprototyp. DieGrundlage der Algorithmen wird ein neues Saturation-Verfahren sein,das vor wenigen Monaten vom ersten Antragsteller und Kollegen entdeckt wurde. Saturation-Verfahren berechnen die Vorgänger oder Nachfolger einergegebenen Menge von Konfigurationen einer abstrakten Maschine. Sie wurden vom zweiten Antragsteller und Kollegen für die Verifikation von Programmen erster Ordung vorgeschlagen, und sind sehr erfolgreich in verschiedenen Werkzeugen implementiert und eingesetzt worden.Insbesondere bilden sie den Kern der Model-Checker MOPED und jMOPED.Das Projekt wird die Erfahrung und Kenntnisse beider Antragsteller kombinieren um diesen Erfolg auf Programme höherer Ordnung zu erweitern.In einer ersten Phase wird das Projekt eine symbolische Version desSaturation-Verfahrens des ersten Antragstellers sowie einen effizientenAlgorithmus zur Berechnung optimaler Gegenbeispiele entwickeln. Neue Ideen sind nötig, da existierende Verfahren für PDA sich auf CPDA nichtdirekt erweitern lassen. Gegenbeispiele sollen in einer zweiten Phase benutzt werden um ein CEGAR-Verfahren (CounterExample Guided Abstraction Refinement) zu entwerfen. Dafür muss Predicate Abstraction für Basistypen um eine neue, zu entwickelnde Secondary Abstraction für höhere Typen erweitert werden. Die dritte und letzte Phase des Projekts wird Algorithmen untersuchen für die Verifikation von Pattern-Matching-Konstrukten, was eine Erweiterung des CPDA-Models erfordert. Wir planen eine Lazy-Abstraktion auf der Basis eines approximierten saturation-Verfahrens zu entwickeln.Jede Phase wird mit einer Leistungsbewertung der neuen Verfahren enden. Fragmente von grossen OCaML und Scala Anwendungen werden alsBenchmarks dienen. Ein ausführlicher Vergleich mit konkurrierenden Methoden soll auch geführt werden.

• DFG-Verfahren: Sachbeihilfen