Title: Symbolic evaluation of imperative programming languages
Language: English
Authors: Burgstaller, Bernd 
Qualification level: Doctoral
Advisor: Blieberger, Johann 
Assisting Advisor: Gramlich, Bernhard
Issue Date: 2005
Number of Pages: 146
Qualification level: Doctoral
Abstract: 
Symbolische Analyse ist eine statische Programmanalysemethode, die Daten- und Kontrollflussinformation an wohldefinierten Programmpunkten beschreibt. Information dieser Art ist von großer Bedeutung für Test und Verifikation von Programmen, sowie für Laufzeitabschätzungen und Programmparallelisierung. Weiters ist symbolische Analyse für optimierende Compiler sowie für Codegeneratoren von Bedeutung.
Gegenstand dieser Dissertation ist ein neuer Ansatz in der symbolischen Analyse, der auf Pfadausdrücken beruht. Pfadausdrücke werden bei diesem Ansatz dazu verwendet, die Kontrollflusseigenschaften eines Programms zu erfassen. Einen wesentlichen Teil der Arbeit stellt jene algebraische Struktur dar, in der die symbolische Analyse stattfindet.
Wir beschreiben Syntax und Semantik einer einfachen Turing-äquivalenten Fluss-Sprache, die uns als Basis für die Definition dieser Struktur dient. In ihrem Mittelpunkt steht der Superkontext, mit dessen Hilfe wir die möglichen Variablenbindungen an einem wohldefinierten Programmpunkt beschreiben.
Um den Seiteneffekt eines Eingabeprogramms zu beschreiben, bilden wir seine einzelnen Programmanweisungen auf Funktionen ab, die ihrerseits einen Superkontext auf einen Superkontext abbilden.
Pfadausdrücke werden sodann im Kontext dieser Funktionen interpretiert, womit wir eine funktionale Beschreibung des Eingabeprogramms erhalten. Ein Korrektheitsbeweis sichert die Richtigkeit dieser funktionalen Beschreibung im Hinblick auf die konkrete Semantik der Fluss-Sprache ab.
Die beschriebene Methode der symbolischen Analyse ist weniger komplex als existierende Methoden, da sie im Wesentlichen aus der Anwendung der funktionalen Programmbeschreibung auf einen Superkontext besteht. Das Ergebnis dieser Funktionsanwendung ist wiederum ein Superkontext, der die Variablenbindungen nach Ausführung des jeweiligen Eingabeprogramms beschreibt.
Die beschriebene Methode kann weiters Lösungen für beliebige Programmpunkte reduzibler sowie irreduzibler Kontrollflussgraphen berechnen und ist damit mächtiger als existierende Methoden.

Symbolic analysis is a static program analysis technique that captures data and control flow information at well-defined program points. This information is useful in the areas of program verification, program testing, worst case execution time analysis, and parallelization. Optimizing compilers and code generators can also benefit from the type of information provided by symbolic analysis.
In this thesis we take a novel approach to symbolic analysis that is based on path expressions.
Path expressions allow us to capture the control flow information that is inherent in a program.
By reinterpreting path expressions we obtain a mapping from the path expression algebra into the symbolic analysis domain.
A major topic of this thesis is therefore the symbolic analysis domain itself. We describe syntax and semantics of a simple yet Turing-equivalent flow language which serves as the basis for the definition of this domain. At the heart of it is the supercontext, an algebraic structure capable of describing all possible variable bindings valid at a well-defined program point.
To describe the computational effects of the input program, we map single statements to functions from supercontexts to supercontexts.
The reinterpretation of path expressions takes place in the context of these functions, thus obtaining a functional description of the input program.
We develop a proof that establishes the correctness of these functional descriptions with respect to the concrete semantics of the flow language.
Our method is less complex than existing methods in the sense that it reduces to the application of the functional description to a given supercontext, yielding a supercontext describing the variable bindings valid after execution of the corresponding input program.
It is more general than existing methods because it can derive solutions for arbitrary graph nodes of reducible and irreducible flow graphs.
Keywords: Programmanalyse; Datenfluss; Kontrollfluss; Methode
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-11235
http://hdl.handle.net/20.500.12708/9621
Library ID: AC04497538
Organisation: E183 - Institut für Rechnergestützte Automation (Automatisierungssysteme. Mustererkennung) 
Publication Type: Thesis
Hochschulschrift
Appears in Collections:Thesis

Files in this item:

Show full item record

Page view(s)

13
checked on Feb 18, 2021

Download(s)

41
checked on Feb 18, 2021

Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.