|
 |
|
 | |  |
| Arbeitsgebiete
Übersetzerbau
Eingebettete Systeme
Formale Semantik von Programmiersprachen
natürliche Semantik
Formale Verifikation
Projekte
Betreute Studien- und Diplomarbeiten
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) |  |  |
 | |  | |  |
| | | |