Kopf der Woche: Dipl.-Ing. Harald Zankl

Dipl.-Ing. Harald Zankl, geboren 1982, schloss im Juni sein Studium der Informatik an der LFU Innsbruck mit Auszeichnung ab.
Dipl.-Ing. Harald Zankl
Bild: Dipl.-Ing. Harald Zankl

In seiner Diplomarbeit "Binary  Decision Diagrams for Precedence-Based Orders" beschäftigte sich Zankl mit der automatischen Terminationsanalyse von Termersetzungssystemen. Diese Systeme bilden die Grundlage der funktionalen Programmierung. Harald Zankl ist der erste Absolvent des Studienzweiges "Informatik" an der LFU Innsbruck.

Das Institut für Informatik wurde 2001 in einer gemeinsamen Initiative der österreichischen Bundesregierung, dem Land Tirol und der Universität Innsbruck gegründet. Das Institut für Informatik stellt das Kernstück einer fundierten IT-Grundlagenforschung dar. Im Wintersemester 2001 begann der erste Lehrbetrieb. Derzeit sind 650 Studierende im Studienzweig "Informatik" eingeschrieben. Jährlich beginnen 100 StudentInnen ein Informatikstudium.

 

Terminationsanalyse von Termersetzungssystemen

In seiner Diplomarbeit beschäftigte sich Zankl mit Terminationsanalysen von Termersetzungssystemen. Im Besonderen untersuchte er die Möglichkeiten der effizienten Implementierung von automatischen Terminationsbeweisern für Termersetzungssysteme.

Das Problem der Termination von Prozessen oder Programmen ist eines der zentralsten Probleme der Informatik. Mit Termersetzungssystemen bezeichnet man ein formales Berechnungsmodell, das die Grundlage der funktionalen Programmierung darstellt. Termersetzungssysteme finden ihre Anwendung unter anderem in der (Terminations-)Analyse von höherstufigen Programmiersprachen, sowie im symbolischen mathematischen Rechnen (beispielsweise im System "Mathematica") und im automatischen Beweisen.

Die von Harald Zankl untersuchten Terminationsmethoden basieren auf der Erkenntnis, dass die traditionell verwendeten Terminationsordnungen als aussagenlogische Probleme kodiert werden können. Die so kodierten Probleme können dann mit effizienten Algorithmen behandelt werden. In der vorgelegten Arbeit wurden die Stärken dieses Ansatzes eindrucksvoll dokumentiert und ausgeweitet.

 

Zur Person

Dipl.-Ing. Harald Zankl wurde am 23.01.1982 in Lienz geboren. Nach seiner Matura am Bundesrealgymnasium Lienz begann er zunächst das Lehramtsstudium Mathematik/Chemie. Im Oktober 2001 war er einer von 400 Erstinskribierten, welche die Möglichkeit wahrnahmen an der LFU Innsbruck den Studienzweig "Informatik" zu studieren. Im Juni 2006 schloss Zankl sein Studium mit Auszeichnung ab. Seine Diplomarbeit schrieb Zankl am Institut für Informatik in der Arbeitsgruppe "Computational Logic", geleitet von Univ.-Prof. Aart Middeldorp. Die von Zankl in seiner Diplomarbeit behandelten Forschungsergebnisse wurden bereits zur Publikation im Rahmen einer internationalen Fachtagung zum Thema "Termination", angenommen.

Zurzeit ist Herr Dipl.-Ing. Zankl im Rahmen des FWF-Projektes "Termination Tools: Verifikation und Optimierung" in der Arbeitsgruppe "Computational Logic" beschäftigt.