Verifizierte Algorithmenanalyse
Final Report Abstract
1. Wir haben eine Bibliothek mathematischer Theorien zur Algorithmenanalyse formalisiert. Mit deren Hilfe konnten wir asymptotische Laufzeitbeweise für divide-and-conquer Algorithmen und für lineare Rekursion automatisieren. Dies war Teil eines umfassenden Programms zur Beweisautomatisierung für asymptotische Aussagen, insb. O(.). 2. Wir haben eine große Bibliothek verifizierter Algorithmen aufgebaut, die verschiedenste Typen von Algorithmen umfasst und von Standardalgorithmen bis zu komplexen, anspruchsvollen Algorithmen wie dem Blossom Algorithmus von Edmonds reicht. Uns ist keine vergleichbar große Bibliothek in einem anderen Theorembeweiser bekannt. 3. Den Bereich der randomisierten Algorithmen haben wir, entgegen der Projektplanung, vernachlässigt und nur wenige (wenn auch komplexe) Algorithmenanalysen verifiziert. 4. Neu hinzu gekommen ist der Bereich KI-Algorithmen, wo wir eine Reihe wichtiger Algorithmen verifizierten, sowohl zur Generierung als auch zur Überprüfung von Lösungen für Plaungs- und Optimierungsprobleme. Die dazugehörigen Veröffentlichungen sind zum großen Teil in KI Konferenzen erschienen, was das Interesse dieser Community an verifizierten Algorithmen demonstriert. 5. Das Thema gewöhnliche Differentialgleichungen und der Lorenz-Attraktor wurde vollständig gelöst: Immler verifizierte einen numerischen Löser für GDGL, wendete ihn auf Tucker’s Lösung des 14. Problems von Smale an und konnte Tucker’s unverifizierte Berechnngen vollständig (und automatisch) verifizieren. 6. Die Monographie Functional Algorithms, Verified! wird als ACM Book erscheinen.
