Automatische Terminierungs- und Komplexitätsanalyse imperativer Programme

• Antragsteller: Professor Dr. Jürgen Giesl
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2013 bis 2025
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 235950644

• Erstellungsjahr: 2024

Zusammenfassung der Projektergebnisse

Die Terminierungs- und Komplexitätsanalyse imperativer Programme ist ein zentraler Punkt der Programmverifikation. Hierzu wurde folgender Ansatz verwendet: Das Front-End erzeugt aus dem Programm einen symbolischen Auswertungsgraph, der alle Programmläufe repräsentiert. Daraus wird ein Programm in einer einfachen Sprache generiert, z.B. ein Termersetzungssystem (TRS) oder ein Integer Transitionssystem (ITS), dessen Terminierung oder Komplexität (im Back-End) untersucht wird. Folgende Resultate wurden erzielt: (A) Terminierungsanalyse: Basierend auf unseren Vorarbeiten zur Terminierung von Java wurde ein Verfahren zur Terminierungsanalyse von C Programmen entwickelt, um sowohl maschinennahe Speicheroperationen als auch Konzepte wie Datenstrukturen, Rekursion und Bitvektor-Zahlen zu behandeln. Während Terminierung im Allgemeinen unentscheidbar ist, wurden Klassen von Programmen identifiziert, bei denen Fragen der Terminierung oder Komplexität entscheidbar sind und entsprechende vollständige Techniken vorgestellt. Zur Verbesserung des Back-Ends wurden mehrere Beiträge zur Terminierung von TRSen entwickelt. Dies betrifft neue Ansätze zur relativen Terminierung und zur “fast sicheren” Terminierung von probabilistischen TRSen sowie den Einsatz der Terminierungsanalyse von TRSen zur Minimierung von Beweisen in Beschreibungslogiken. (B) Komplexitätsanalyse (Obere Schranken): Terminierungs-Techniken lassen sich modifizieren, um damit obere Schranken für die Laufzeit von Programmen zu berechnen. Dies betrifft sowohl die Front-Ends für Java und C also auch die Back-Ends für TRSe und ITSe. Insbesondere wurde ein modulares Verfahren zur Komplexitätsanalyse von ITSen entwickelt, das Schranken für die Laufzeit und die Werte der Programmvariablen für einzelne Teilprogramme berechnet. Um seine Mächtigkeit zu erhöhen, wurden vollständige Verfahren für Teilprogramme mit berechenbaren Schranken (wie in (A)) integriert. Der Ansatz wurde auch auf die Berechnung erwarteter Laufzeitschranken für probabilistische ITSe erweitert. (C) Komplexitätsanalyse (Untere Schranken): Zur Fehlersuche wurden Techniken zur Berechnung unterer Laufzeitschranken für Back-End Programme entwickelt. Für ITSe beruhen diese auf einer Loop Acceleration, die Schleifen in nichtdeterministische Instruktionen übersetzt. Hierzu wurden neue Kalküle vorgestellt, die Loop Acceleration mit der Suche nach Gegenbeispielen verbinden. Diese lassen sich auch für NichtTerminierungsbeweise und zur Erfüllbarkeitsanalyse von Constraint Horn Clauses verwenden (um Sicherheitseigenschaften von Programmen zu untersuchen). Da Loop Acceleration oft exponentielle Ausdrücke erzeugt, wurde auch eine entsprechende Erweiterung von SMT Solvern entwickelt. (D) Implementierung: Alle Resultate wurden in unseren Tools AProVE (für den Gesamt-Ansatz), KoAT und LoAT (für obere und untere Schranken bei ITSen) und SwInE (für SMT modulo exponentieller Arithmetik) implementiert und in umfangreichen Experimenten und Wettbewerben evaluiert.

Link zum Abschlussbericht

https://doi.org/10.34657/17569

Projektbezogene Publikationen (Auswahl)

• Termination of Polynomial Loops. Lecture Notes in Computer Science, 89-112.
  Frohn, Florian; Hark, Marcel & Giesl, Jürgen
  
• Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes. Lecture Notes in Computer Science, 250-269.
  Meyer, Fabian; Hark, Marcel & Giesl, Jürgen
  
• A calculus for modular loop acceleration and non-termination proofs. International Journal on Software Tools for Technology Transfer, 24(5), 691-715.
  Frohn, Florian & Fuhs, Carsten
  
• AProVE: Non-Termination Witnesses for C Programs. Lecture Notes in Computer Science, 403-407.
  Hensel, Jera; Mensendiek, Constantin & Giesl, Jürgen
  
• Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops. Lecture Notes in Computer Science, 734-754.
  Lommen, Nils; Meyer, Fabian & Giesl, Jürgen
  
• Improving Automatic Complexity Analysis of Integer Programs. Lecture Notes in Computer Science, 193-228.
  Giesl, Jürgen; Lommen, Nils; Hark, Marcel & Meyer, Fabian
  
• Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description). Lecture Notes in Computer Science, 712-722.
  Frohn, Florian & Giesl, Jürgen
  
• ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses. Lecture Notes in Computer Science, 259-285.
  Frohn, Florian & Giesl, Jürgen
  
• Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs. Lecture Notes in Computer Science, 344-364.
  Kassing, Jan-Christoph & Giesl, Jürgen
  
• Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper). Lecture Notes in Computer Science, 220-233.
  Frohn, Florian & Giesl, Jürgen
  
• Proving Termination of C Programs with Lists. Lecture Notes in Computer Science, 266-285.
  Hensel, Jera & Giesl, Jürgen
  
• Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs. Lecture Notes in Computer Science, 3-22.
  Lommen, Nils & Giesl, Jürgen
  
• A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting. Lecture Notes in Computer Science, 62-80.
  Kassing, Jan-Christoph; Dollase, Stefan & Giesl, Jürgen
  
• A Dependency Pair Framework for Relative Termination of Term Rewriting. Lecture Notes in Computer Science, 360-380.
  Kassing, Jan-Christoph; Vartanyan, Grigory & Giesl, Jürgen
  
• Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper). Lecture Notes in Computer Science, 233-243.
  Lommen, Nils; Meyer, Éléanore & Giesl, Jürgen
  
• F. Baader and J. Giesl. On the complexity of the small term reachability problem for terminating term rewriting systems. In Proc. FSCD ’24, LIPIcs, 2024
  F. Baader & J. Giesl
  
• From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting. Lecture Notes in Computer Science, 206-228.
  Kassing, Jan-Christoph; Frohn, Florian & Giesl, Jürgen
  
• Integrating Loop Acceleration Into Bounded Model Checking. Lecture Notes in Computer Science, 73-91.
  Frohn, Florian & Giesl, Jürgen
  
• Satisfiability Modulo Exponential Integer Arithmetic. Lecture Notes in Computer Science, 344-365.
  Frohn, Florian & Giesl, Jürgen