Arbeitsgebiete

Ausführliche Informationen finden Sie auf meiner Webseite http://www.info.uni-karlsruhe.de/~glesner

Projekte

Abgeschlossen Aktionsplan Informatik CRS Eliteförderprogramm für Postdoktoranden Verifix

Betreute Studien- und Diplomarbeiten

		Diplomarbeit
		Befehlsauswahl auf SSA-Graphen (abgeschlossen)
		Codegenerierung für digitale Signalprozessoren (abgeschlossen)
		Eine formale Semantik für den Pi-Kalkül (abgeschlossen)
		Eine formale Semantik für SSA-Zwischensprachen in Isabelle/HOL (abgeschlossen)
		Eine strukturell operationale Semantik für static-single-assignment Sprachen (abgeschlossen)
		Graphersetzung für Optimierungen in der Codeerzeugung (abgeschlossen)
		Studienarbeit
		Checker für Konstantenpropagierung in Compilern (abgeschlossen)
		Codeerzeugung aus Firm mit dem lcc-Backend (abgeschlossen)
		Ein Programm-Ergebnis-Prüfer für die syntaktische Analyse des GCC Compilers (abgeschlossen)
		Entwurf und Implementierung einer Schnittstelle für SSA-Sprachen (abgeschlossen)
		Evaluierung graphersetzungsbasierter Optimierungen (abgeschlossen)
		Generierung von .NET IL Assembler aus Firm (abgeschlossen)
		Koalgebraische Methoden in der maschinellen Verifikation vonoptimierenden Programmtransformationen (abgeschlossen)
		Maschinelle Verifikation der Codeerzeugung für VLIW-Prozessoren (abgeschlossen)
		Maschinelle Verifikation der Eliminierung toten Codes in SSA-Darstellungen (abgeschlossen)
		Spezifikation und maschinelle Verifikation von Konstantenfaltung in Compiler Backends (abgeschlossen)
		The Sherlock-System (abgeschlossen)
		Verifikation unimodularer Schleifentransformationen (abgeschlossen)

Veröffentlichungen

		2005
		Blech, Glesner, Leitner, Formal Verification of Java Code Generation from UML Models
		Glesner, An Introduction to (Co)Algebras and (Co)Induction and their Application to the Semantics of Programming Languages
		Blech, Gesellensetter, Glesner, Formal Verification of Dead Code Elimination in Isabelle/HOL
		Blech, Glesner, Leitner, Mülling, A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL
		Glesner, Blech, Logische und softwaretechnische Herausforderungen bei der Verifikation optimierender Compiler
		2004
		Glesner, Goos, Zimmermann, Verifix: Konstruktion und Architektur verifizierender Ãœbersetzer (Verifix: Construction and Architecture of Verifying Compilers)
		Blech, Glesner, A Formal Correctness Proof for Code Generation from SSA Form in Isabelle/HOL
		Glesner, Zimmermann, Natural Semantics as a Static Program Analysis Framework
		Glesner, Forster, Jäger, A Program Result Checker for the Lexical Analysis of the GNU C Compiler
		Glesner, A Proof Calculus for Natural Semantics Based on Greatest Fixed Point Semantics
		Glesner, An ASM Semantics for SSA Intermediate Representations
		2003
		Glesner, Program Checking with Certificates: Separating Correctness-Critical Code
		Glesner, Using Program Checking to Ensure the Correctness of Compiler Implementations
		Glesner, Blech, Classifying and Formally Verifying Integer Constant Folding
		Glesner, ASMs versus Natural Semantics: A Comparison with New Insights
		2002
		Glesner, Geiß, Boesler, Verified Code Generation for Embedded Systems
		2001
		Glesner, Zimmermann, Structural Simulation Proofs based on ASMs even for Non-Terminating Programs
		1999
		Glesner, Natürliche Semantik für imperative und objektorientierte Programmiersprachen
		Glesner, Stroetmann, Combining Inclusion Polymorphism and Parametric Polymorphism
		Glesner, Natural Semantics for Imperative and Object-Oriented Programming Languages
		1998
		Glesner, Many-Sorted Natural Semantics - Specification and Generation of the Semantic Analysis for Imperative and Object-Oriented Programming Languages
		Glesner, Zimmermann, Using Many-Sorted Natural Semantics to Specify and Generate Semantic Analysis
		1997
		Glesner, Zimmermann, Using Many-Sorted Inference Rules to Generate Semantic Analysis
		Kolbe, Glesner, Many-Sorted Logic in a Learning Theorem Prover
		1996
		Glesner, Mehrsortige Logik in einem Lernenden Beweiser
		1995
		Glesner, Koller, Constructing Flexible Dynamic Belief Networks from First-Order Probabilistic Knowledge Bases
		1994
		Glesner, Constructing Flexible Dynamic Belief Networks from First-Order Probabilistic Knowledge Bases (Master's Thesis)