Automatische Terminierungsanalyse für funktionale, imperative und logische Programmiersprachen
Final Report Abstract
Unser Ziel war die Entwicklung von Verfahren, um die Terminierung von Programmen automatisch nachzuweisen. Unsere Arbeitshypothese war, dass die grundlegende Aufgabe der Terminierungsanalyse unabhängig von der Programmiersprache ist. Um Programme verschiedener Sprachen zu analysieren, werden sie daher in Terminierungsprobleme eines gemeinsamen Basisformalismus transformiert. Hierfür wurde die Sprache der Termersetzungssysteme gewählt, deren Terminierung seit Jahrzehnten intensiv untersucht wird und für die zahlreiche Terminierungstechniken und Tools verfügbar sind. Insbesondere ist hier das von uns im Projekt mit entwickelte Dependency Pair Framework zu nennen, das in praktisch allen dieser Tools integriert ist. In den ersten Projektphasen wurde die Tragfähigkeit dieses Ansatzes gezeigt und Verfahren zur automatischen Terminierungsanalyse für die funktionale Programmiersprache Haskell, die objektorientierte imperative Sprache Java und die logische Programmiersprache Prolog entwickelt. Der momentane Berichtszeitraum stellt die dritte Phase des Projekts dar. Hier wurden folgende Resultate entwickelt, die in führenden internationalen Zeitschriften und Konferenzen veröffentlicht wurden. (A) Die automatischen Transformationen von Programmen in Termersetzungssysteme wurden erweitert, so dass auch aus Programmen mit komplexen Konzepten Termersetzungssysteme entstehen, die für die automatische Terminierungsanalyse geeignet sind. Hierbei wurden Sprachen verschiedener Programmierparadigmen betrachtet: (A.1) Zur Integration unserer Terminierungsverfahren in allgemeine Verifikationstools wurde untersucht, wie unser Ansatz mit einem Theorembeweiser wie Isabelle gekoppelt werden kann, bei dem Programme auf funktionale Weise spezifiziert werden. (A.2) Unser Verfahren zur Terminierungsanalyse von Java wurde grundlegend erweitert (um die Behandlung zyklischer Objekte, die Analyse rekursiver Methoden und um die Mäglichkeit, auch die Nicht-Terminierung von Methoden nachzuweisen. (A.3) Unser Ansatz zur Terminierungsanalyse von Prolog wurde durch Verwendung einer neuen Semantik um zahlreiche Konzepte der Sprache erweitert und in seiner Mächtigkeit deutlich verbessert. Außerdem wurde er so adaptiert, dass er nun auch zur Komplexitätsanalyse von Prolog-Programmen verwendbar ist. (B) Die Leistungsstarke unserer Techniken für Termersetzungssysteme wurde signifikant verbessert, um die Terminierung und die Laufzeit der Systeme zu analysieren, die aus Programmen der verschiedenen Sprachen entstehen. Hierbei wurden folgende Beiträge entwickelt: (B.1) Steigerung der Effizienz und Machtigkeit der Terminierungsanalyse durch geeignete SAT-Codierungen und durch die Kopplung verschiedener Techniken. (B.2) Verbesserte Verfahren zum Nachweis der Nicht-Terminierung (B.3) Einsatz von Terminierungstechniken zur automatischen Komplexitätsanalyse (C) Die Resultate aus (A) und (B) wurden in unserem Verifikationstool AProVE implementiert und in umfangreichen Experimenten evaluiert. Das Tool ist unter http://aprove. informatik.rwth-aachen.de äber ein Web-Interface verfügbar, das die Terminierungsanalyse für Haskell-, Java- und Prolog-Programme sowie für Termersetzungssysteme ermöglicht. Daräber hinaus erlaubt es eine Reproduktion unserer Experimente, die unter http://aprove. informatik.rwth-aachen.de/eval/#experiments detailliert beschrieben werden. Die Ergebnisse des Projekts zeigen, dass Termersetzungstechniken in der Tat zur automatischen Terminierungsanalyse von Programmen in realen praxisrelevanten Programmiersprachen geeignet sind. Dies wird auch in der jährlichen internationalen Termination Competition deutlich, bei der sich AProVE als das mächtigste System für die Terminierungsanalyse von Haskell-, Java- und Prolog-Programmen sowie von Termersetzungssystemen erwiesen hat.
Publications
- Mechanizing and improving dependency pairs. Journal of Automated Reasoning, 37(3): 155–203. Springer-Verlag, 2006
J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke
- Automated termination proofs for logic programs by term rewriting. ACM Transactions on Computational Logic, 11(1):2/1–2/52, 2009.
P. Schneider-Kamp, J. Giesl, A. Serebrenik, and R. Thiemann
- Proving termination of integer term rewriting. In Proc. RTA ’09, LNCS 5595, pages 32–47. Springer-Verlag, 2009
C. Fuhs, J. Giesl, M. Plücker, P. Schneider-Kamp, and S. Falke
- Automated termination analysis for logic programs with cut. In Proc. ICLP ’10, Theory and Practice of Logic Programming, 10(4–6):365–381. Cambridge University Press, 2010
P. Schneider-Kamp, J. Giesl, T. Ströder, A. Serebrenik, and R. Thiemann
- A dependency pair framework for innermost complexity analysis of term rewrite systems. In Proc. CADE ’11, LNAI 6803, pages 422–438. Springer-Verlag, 2011. Revised extended version to appear in the Journal of Automated Reasoning
L. Noschinski, F. Emmes, and J. Giesl
- Automated termination proofs for Haskell by term rewriting. ACM Transactions on Programming Languages and Systems, 33(2):7/1–7/39, 2011
J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, and R. Thiemann
- Modular termination proofs of recursive Java Bytecode programs by term rewriting. In Proc. RTA ’11, LIPIcs 10, pages 155–170. Dagstuhl Publishing, 2011
M. Brockschmidt, C. Otto, and J. Giesl
- Automated termination proofs for Java programs with cyclic data. In Proc. CAV ’12, LNCS 7358, pages 105–122. Springer-Verlag, 2012
M. Brockschmidt, R. Musiol, C. Otto, and J. Giesl
- SAT solving for termination proofs with recursive path orders and dependency pairs. Journal of Automated Reasoning, 49(1):53–93. Springer- Verlag, 2012
M. Codish, J. Giesl, P. Schneider-Kamp, and R. Thiemann
(See online at https://doi.org/10.1007/s10817-010-9211-0) - Symbolic evaluation graphs and term rewriting – A general methodology for analyzing logic programs. In Proc. PPDP ’12, pages 1-12. ACM Press, 2012
J. Giesl, T. Str¨der, P. Schneider-Kamp, F. Emmes, and C. Fuhs
