Sabine Glesner's Publications

Theses

• Sabine Glesner. Verification of Optimizing Compilers. Habilitationsschrift, Fakultät für Informatik, Universität Karlsruhe, November 2004.
• Sabine Glesner. Natürliche Semantik für imperative und objektorientierte Programmiersprachen. PhD Thesis, Fakultät für Informatik, Universität Karlsruhe, February 1999. Shaker Verlag Aachen, ISBN: 3-8265-6388-3, 1999.
• Sabine Glesner. Mehrsortige Logik in einem Lernenden Beweiser. Diplomarbeit, Fachbereich Informatik, Technische Hochschule Darmstadt, 1996.
• Sabine Glesner. Constructing Flexible Dynamic Belief Networks from First-Order Probabilistic Knowledge Bases. Master's thesis, Department of Electrical Engineering and Computer Science, University of California, Berkeley, 1994.

Journal Articles

• Sabine Glesner and Wolf Zimmermann: Natural Semantics as a Static Program Analysis Framework. In ACM Transactions on Programming Languages and Systems, Vo. 26, No. 3, pages 510-577, May 2004.
Preversion.
• Sabine Glesner, Gerhard Goos, and Wolf Zimmermann: Verifix: Konstruktion und Architektur verifizierender Übersetzer. it - information technology, Vol. 46, Issue 5/2004, pages 265-276, 2004.
• Sabine Glesner: Using Program Checking to Ensure the Correctness of Compiler Implementations. In Journal of Universal Computer Science (J.UCS), Vol. 9, No. 3, pages 191-222, March 2003. Preversion.

Refereed Papers

• Jan Olaf Blech, Lars Gesellensetter, and Sabine Glesner: Formal Verification of Dead Code Elimination in Isabelle/HOL. In 3rd IEEE International Conference on Software Engineering and Formal Methods, IEEE Computer Society Press, Koblenz, Germany, September 2005.
• Jan Olaf Blech, Sabine Glesner, and Johannes Leitner: Formal Verification of Java Code Generation from UML Models. In Proceedings of the 3rd International Fujaba Days, Technical Report, University of Paderborn, 2005.
• Jan Olaf Blech, Sabine Glesner, Johannes Leitner, and Steffen Mülling: Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL. In Proceedings of the COCV-Workshop (Compiler Optimization meets Compiler Verification), 8th European Conferences on Theory and Practice of Software (ETAPS 2005), Edinburgh, Scotland, April 2005, accepted for publication in Electronic Notes in Theoretical Computer Science (ENTCS).
• Sabine Glesner and Jan Olaf Blech: Logische und softwaretechnische Herausforderungen bei der Verifikation optimierender Compiler. In Proceedings der Tagung Software Engineering 2005, Essen, Germany, 2005, Lecture Notes in Informatics.
• Jan Olaf Blech and Sabine Glesner: A Formal Correctness Proof for Code Generation from SSA Form in Isabelle/HOL. In Proceedings der 3. Arbeitstagung Programmiersprachen (ATPS) auf der 34. Jahrestagung der Gesellschaft für Informatik, Ulm, Germany, 2004, Lecture Notes in Informatics.
• Sabine Glesner: An ASM Semantics for SSA Intermediate Representations. In Proceedings of the 11th International Workshop on Abstract State Machines, Wittenberg, Germany, Mai 2004. Springer Verlag, Lecture Notes in Computer Science, Vol. 3052, ISBN: 3-540-22094-1.
• Sabine Glesner: A Proof Calculus for Natural Semantics Based on Greatest Fixed Point Semantics. In Proceedings of the COCV-Workshop (Compiler Optimization meets Compiler Verification), 7th European Conferences on Theory and Practice of Software (ETAPS 2004), Barcelona, Spain, April 2004, accepted for publication in Electronic Notes in Theoretical Computer Science (ENTCS).
• Sabine Glesner, Simone Forster, and Matthias Jäger: A Program Result Checker for the Lexical Analysis of the GNU C Compiler. In Proceedings of the COCV-Workshop (Compiler Optimization meets Compiler Verification), 7th European Conferences on Theory and Practice of Software (ETAPS 2004), Barcelona, Spain, April 2004, accepted for publication in Electronic Notes in Theoretical Computer Science (ENTCS).
• Sabine Glesner: Program Checking with Certificates: Separating Correctness-Critical Code. In Proceedings of the 12th International FME Symposium (Formal Methods Europe), editors Keijiro Araki, Stefania Gnesi, Dino Mandrioli, Pisa, Italy, September 2003. Springer Verlag Lecture Notes in Computer Science, Vol. 2805, pages 758-777.
• Sabine Glesner. ASMs versus Natural Semantics: A Comparison with New Insights. In Proceedings of the 9th International Workshop on Abstract State Machines ASM 2003, Springer Verlag, Lecture Notes in Computer Science, Vol. 2589, pages 293-308, Italy, March 2003.
• Sabine Glesner and Jan Olaf Blech: Classifying and Formally Verifying Integer Constant Folding. In Proceedings of the COCV-Workshop (Compiler Optimization meets Compiler Verification), 6th European Conferences on Theory and Practice of Software (ETAPS 2003), Electronic Notes in Theoretical Computer Science (ENTCS), Vol. 82, No. 2, Warsaw, Poland, April 12, 2003.(Long version including Isabelle proof)
• Sabine Glesner, Rubino Geiß, and Boris Boesler. Verified Code Generation for Embedded Systems. In Proceedings of the COCV-Workshop (Compiler Optimization meets Compiler Verification), 5th European Conferences on Theory and Practice of Software (ETAPS 2002), Electronic Notes in Theoretical Computer Science (ENTCS), Vol. 65, No. 2, Grenoble, April 13, 2002.
• Sabine Glesner. Natural Semantics for Imperative and Object-Oriented Programming Languages. In Proceedings der 29. Jahrestagung der Gesellschaft für Informatik, Arbeitstagung Programmiersprachen '99, Springer Verlag, 1999.
• Sabine Glesner and Wolf Zimmermann. Using Many-Sorted Natural Semantics to Specify and Generate Semantic Analysis. In Proceedings of the Systems Implementation Conference (SI2000), organized by IFIP Working Group 2.4, Chapman & Hall, 1998.
• Thomas Kolbe and Sabine Glesner. Many-Sorted Logic in a Learning Theorem Prover. In Proceedings of the 21st German Annual Conference on Artificial Intelligence (KI '97), Freiburg, Germany, September 1997. Springer Verlag 1997 (LNCS).
• Sabine Glesner and Daphne Koller. Constructing Flexible Dynamic Belief Networks from First-Order Probabilistic Knowledge Bases,.In Proceedings of the European Conference on Symbolic and Quantitative Approaches to Reasoning under Uncertainty (ECSQARU '95), Fribourg, Switzerland, July 1995. In Lecture Notes in Artificial Intelligence, Ch. Froidevaux and J. Kohlas (Eds.), Springer Verlag, 1995, pages 217-226.