Universitńt Karlsruhe
Prof. Dr. rer. nat. Sabine Glesner

Arbeitsgebiete

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


├ťbersetzerbau
Eingebettete Systeme
Formale Semantik von Programmiersprachen
nat├╝rliche Semantik
Formale Verifikation

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)
Login
Links