Research interests

Please have also a look at the detailed information on my website http://www.info.uni-karlsruhe.de/~glesner

Projects

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

Advised thesis subjects

		Diploma thesis
		A Formal Semantics for SSA Intermediate Representations in Isabelle/HOL (closed)
		A Formal Semantics for the Pi Calculus (closed)
		A Structural Operational Semantics for Static-Single-Assignment Languages (closed)
		Code Generation for Digital Signal Processors (closed)
		Graph transformation based optimizations in compiler backends (closed)
		Instruction selection on SSA-graphs (closed)
		Studien thesis
		(see german version) (closed)
		A Program Result Checker for the Syntactic Analysis of the GCC Compiler (closed)
		Checker for Constant Propagation in Compilers (closed)
		Coalgebraic Methods in Verification of optimizing Program transformations using Theorem provers (closed)
		Evaluierung graphersetzungsbasierter Optimierungen (closed)
		Generating .NET IL Assembler from FIRM (closed)
		Maschinelle Verifikation der Codeerzeugung für VLIW-Prozessoren (closed)
		Mechanical Verification of Dead Code Elimination in SSA Representations (closed)
		Specification and Mechanical Verification of Constant Folding in Compiler Backends (closed)
		The Sherlock-System (closed)
		Verifikation unimodularer Schleifentransformationen (closed)

Publications

		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)