h1

h2

h3

h4

h5
h6

DFG project G:(GEPRIS)235950644

Automatische Terminierungs- und Komplexitätsanalyse imperativer Programme

CoordinatorProfessor Dr. Jürgen Giesl
Grant period2013 - 2024
Funding bodyDeutsche Forschungsgemeinschaft
 DFG
IdentifierG:(GEPRIS)235950644

Note: Das Ziel ist die Entwicklung von Techniken zur automatischen Terminierungs- und Komplexitätsanalyse von imperativen Programmen in Sprachen wie Java und C. Solche Techniken sindbeim Entwurf und der Verifikation von Programmen von zentraler Bedeutung. In der ersten Phase des Projekts wurde hierzu der folgende Ansatz entwickelt: Zunächst wird (im Front-End des Verfahrens) automatisch ein symbolischer Auswertungsgraph erzeugt, der alle möglichen Läufe des Java- oder C-Programms repräsentiert. Aus diesem Graph wird anschließend ein Programm in einer einfachen Sprache (wie z.B. ein Integer Transitionssystem oder ein Termersetzungssystem) generiert, dessen Terminierung oder Komplexität dann (im Back-End) untersucht wird. Die Ergebnisse der ersten Phase des Projekts zeigen den Erfolg des Ansatzes. In der zweiten Phase soll der Ansatz zu einem praktisch verwendbaren Verfahren weiterentwickelt werden. Dazu sollen im Vorhaben folgende Ziele verfolgt werden: (A) Es existieren wichtige Klassen von Programmen, bei denen die bislang entwickelten Techniken zum Nachweis der Terminierung nicht verwendet werden können. Daher sollen diese Techniken entsprechend erweitert und so modularisiert werden, dass sie auch für große Programme einsetzbar werden. (B) Die Techniken zum Terminierungsnachweis lassen sich so modifizieren, dass damit auch obere Komplexitätsschranken für die Laufzeit von Programmen berechnet werden können. Der in der ersten Projektphase entwickelte Ansatz führt allerdings oft noch zu sehr hohen Schranken, so dass die Präzision und die Einsetzbarkeit des Verfahrens daher deutlich verbessert werden sollen. (C) Darüber hinaus wurden in der ersten Projektphase auch Techniken zur automatischen Berechnung unterer Komplexitätsschranken für die Laufzeit der Back-End Programme entwickelt. Die Aufgabe ist nun,diese Verfahren so weiterzuentwickeln, dass sie auch für Sprachen wie Java und C im Front-End einsetzbar werden. (D) Um ihre Leistungsfähigkeit zu überprüfen, sollen die in (A) – (C) entwickelten Verfahren in unseren Verifikationstools AProVE, KoAT und LoAT implementiert und durch umfangreiche Experimente empirisch evaluiert und mit anderen Systemen verglichen werden.
   

Recent Publications

All known publications ...
Download: BibTeX | EndNote XML,  Text | RIS | 

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Journal Article  ;
Small Term Reachability and Related Problems for Terminating Term Rewriting Systems
Logical methods in computer science : LMCS 21(4), 14938 () [10.46298/lmcs-21(4:8)2025]  GO DBCoverage BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Journal Article/Contribution to a conference proceedings  ;  ;
Termination of triangular polynomial loops
Static Analysis Symposium, SAS 2020 & 2022, Meeting location, Formal methods in system design 65(1), 70-132 () [10.1007/s10703-023-00440-z] special issue: "Special Issue on 'Static Analysis Symposium (SAS) 2020 & 2022'"  GO BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;
Integrating Loop Acceleration Into Bounded Model Checking
Formal methods : 26th international symposium, FM 2024, Milan, Italy, September 9-13, 2024, proceedings / André Platzer, Kristin Yvonne Rozier, Matteo Pradella Matteo Rossi, editors. - Part I
26. International Symposium on Formal Methods, FM 2024, MilanMilan, Italy, 9 Sep 2024 - 13 Sep 20242024-09-092024-09-13 Cham : Springer, Lecture notes in computer science 14933, 73-91 () [10.1007/978-3-031-71162-6_4]  GO OpenAccess  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;
On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems
9th International Conference on Formal Structures for Computation and Deduction : FSCD 2024, July 10-13, 2024, Tallinn, Estonia / edited by Jakob Rehof
9. International Conference on Formal Structures for Computation and Deduction, FSCD 2024, TallinnTallinn, Estonia, 10 Jul 2024 - 13 Jul 20242024-07-102024-07-13 Saarbrücken/Wadern, Germany : Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, June, Leibniz international proceedings in informatics 299, 16:1-16:18 () [10.4230/LIPICS.FSCD.2024.16]  GO OpenAccess  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;  ;
A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting
Functional and logic programming : 17th international symposium, FLOPS 2024, Kumamoto, Japan, May 15-17, 2024 : proceedings / Jeremy Gibbons, Dale Miller, editors
17. International Symposium on Functional and Logic Programming, FLOPS 2024, KumamotoKumamoto, Japan, 15 May 2024 - 17 May 20242024-05-152024-05-17 Singapore : Springer, Lecture notes in computer science 14659, 62-80 () [10.1007/978-981-97-2300-3_4]  GO BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;  ;
From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting
Foundations of software science and computation structures : 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024 : Proceedings/ Naoki Kobayashi, James Worrell editors. - Part 2
27. International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2024, Luxembourg CityLuxembourg City, Luxembourg, 8 Apr 2024 - 11 Apr 20242024-04-082024-04-11
European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg CityLuxembourg City, Luxembourg, 8 Apr 2024 - 11 Apr 20242024-04-082024-04-11 Cham, Switzerland : Springer, Lecture Notes in Computer Science 14575, 206-228 () [10.1007/978-3-031-57231-9_10]  GO OpenAccess  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;
Satisfiability Modulo Exponential Integer Arithmetic
Automated reasoning : 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings / Christoph Benzmüller, Marijn J.H. Heule, Renate A. Schmidt editors. - Part 1
12. International Joint Conference on Automated Reasoning, IJCAR 2024, NancyNancy, France, 3 Jul 2024 - 6 Jul 20242024-07-032024-07-06 Cham, Switzerland : Springer, Lecture notes in computer science 14739, Lecture notes in artificial intelligence 344-365 () [10.1007/978-3-031-63498-7_21]  GO OpenAccess  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;  ;
Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper)
Automated reasoning : 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings / Christoph Benzmüller, Marijn J.H. Heule, Renate A. Schmidt editors. - Part 1
12. International Joint Conference on Automated Reasoning, IJCAR 2024, NancyNancy, France, 3 Jul 2024 - 6 Jul 20242024-07-032024-07-06 Cham, Switzerland : Springer, Lecture notes in computer science 14739, Lecture notes in artificial intelligence 233-243 () [10.1007/978-3-031-63498-7_14]  GO OpenAccess  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;  ;
A Dependency Pair Framework for Relative Termination of Term Rewriting
Automated reasoning : 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024 : proceedings/ Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt editors. - Part 2
12. International Joint Conference on Automated Reasoning, IJCAR 2024, NancyNancy, France, 3 Jul 2024 - 6 Jul 20242024-07-032024-07-06 Cham, Switzerland : Springer, Lecture notes in computer science 14740, Lecture notes in artificial intelligence 360-380 () [10.1007/978-3-031-63501-4_19]  GO OpenAccess  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;
ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses
Static Analysis : 30th International Symposium, SAS 2023, Cascais, Portugal, October 22–24, 2023, Proceedings / edited by Manuel V. Hermenegildo, José F. Morales
30. International Static Analysis Symposium, SAS 2023, CascaisCascais, Portugal, Cham : Springer Nature Switzerland, Lecture Notes in Computer Science 14284, 259-285 () [10.1007/978-3-031-44245-2_13]  GO BibTeX | EndNote: XML, Text | RIS

All known publications ...
Download: BibTeX | EndNote XML,  Text | RIS | 

 Datensatz erzeugt am 2022-09-01, letzte Änderung am 2024-09-26
Ähnliche Datensätze



Dieses Dokument bewerten:

Rate this document:
1
2
3
4
5
 
(Bisher nicht rezensiert)