Titelaufnahme

Titel
Resource Bound-Analyse von Lisp-Programmen / von Clemens Danninger
Weitere Titel
Resource bound analysis of Lisp programs
Verfasser / Verfasserin Danninger, Clemens Florian
Begutachter / BegutachterinSinn, Moritz ; Zuleger, Florian
ErschienenWien, 2016
Umfangxiii, 92 Seiten
HochschulschriftTechnische Universität Wien, Diplomarbeit, 2016
Anmerkung
Zusammenfassung in deutscher Sprache
Text in englischer Sprache
Anmerkung
Abweichender Titel nach Übersetzung der Verfasserin/des Verfassers
SpracheEnglisch
DokumenttypDiplomarbeit
Schlagwörter (DE)Ressourcenanalyse / Automatische Boundanalyse / Statische Analyse / Programmanalyse / Komplexitätsanalyse
Schlagwörter (EN)Resource Analysis / Automatic Bound Analysis / Static Analysis / Program Analysis / Complexity Analysis
URNurn:nbn:at:at-ubtuw:1-110432 Persistent Identifier (URN)
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
Resource Bound-Analyse von Lisp-Programmen [0.49 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Deutsch)

Resource Bound Analysis ist ein Bereich der Programmanalyse, der sich mit der Bestimmung von Bounds (Grenzen) für die Menge an bestimmten Ressourcen, die beim Durchlauf eines Programms verbraucht werden, beschäftigt. Bounds sind Ausdrücke über die Eingabeparameter eines Programms, die für beliebige Kombinationen von Parametern korrekt sein sollten, was durch einfaches Testen nicht erreichbar ist. Die Analysetypen, die hier behandelt werden, sind statisch (d.h. es ist nicht notwendig, das Programm auszuführen, um einen Bound zu bestimmen) und vollständig automatisiert. Bounds für viele verschiedene Arten von Ressourcen sind von Interesse, darunter Laufzeit, Stack und Heap-Ausnutzung oder wie oft eine bestimmte Funktion aufgerufen wird. Resource Bound Analysis hat zahlreiche Anwendungsmöglichkeiten in der Entwicklung von Embedded- und Echtzeitsystemen, Komplexitätsanalyse von Algorithmus-Implementierungen, Security und weiteren, die wir detaillierter beschreiben. Viele neuere Ansätze und Implementierungen zielen auf imperative Programme ab. Im Gegensatz dazu konzentriert sich diese Arbeit auf funktionale Programme, wo Wiederholung (der wichtigste Aspekt in der Resource Bound Analysis) als rekursive Funktionsaufrufe statt als Schleifen implementiert ist. Da Ressourcenanalyse ein umfangreiches und komplexes Thema ist, beschränken wir unsere Analyse auf die Berechnung von Bounds für die Anzahl an Funktionsaufrufen und damit, wie oft jeder Teil des Programms ausgeführt wird. Wir legen allerdings dar, dass damit das Kernproblem gelöst ist und eine Erweiterung auf andere Ressourcentypen auf dieser Grundlage relativ einfach wäre. Wir präsentieren eine Boundanalyse für eine seiteneffektfreie Untermenge von Common Lisp mit Funktionen erster Ordnung. Die Analyse baut auf CoFloCo auf, einem existierenden Boundanalysesystem, das Bounds aus einem System von Cost Relations berechnet. Wir beschreiben eine Übersetzung von Lisp in Cost Relations, die die Berechnung korrekter Bounds für Lisp-Programme mit polynomieller Komplexität ermöglicht. Wir berichten über Experimente, die mit einem umfangreichen Benchmark durchgeführt wurden, das aus zusammen mit dem Theorembeweiser ACL2 verteilten Lisp-Programmen besteht. Insgesamt analysierten wir 19,491 Funktionen in 1,934 Dateien. Das Benchmark enthält Code für Modelle, die für Theorembeweise in industriellen Anwendungen wie etwa Hardware- und Mikrocodeverifikation verwendet wurden. Dasselbe Benchmark wurde außerdem bereits für die Evaluation des Terminationsbeweisers CCG verwendet, der in ACL2 enthalten ist. Wir untersuchen die erhaltenen Bounds und asymptotischen Komplexitätsergebnisse sowie die Laufzeit der Analyse als wichtigen Aspekt für praktische Anwendungen von Programmanalyse, um die Eignung unseres Ansatzes zu beurteilen und verbleibende (technische wie fundamentale) Probleme zu identifizieren.

Statistik
Das PDF-Dokument wurde 15 mal heruntergeladen.