Publications

Sabine Glesner and Daphne Koller (1995). Constructing Flexible Dynamic Belief Networks from First-Order Probabilistic Knowledge Bases. Proceedings of the European Conference on Symbolic and Quantitative Approaches to Reasoning under Uncertainty (ECSQARU. Springer Verlag, Lecture Notes in Artificial Intelligence, 217-226.

Sabine Glesner and Wolf Zimmermann (1997). Using Many-Sorted Inference Rules to Generate Semantic Analysis. Proceedings des Workshops der Informatik- Graduiertenkollegs "Promotion tut not: Innovationsmotor Graduiertenkolleg" im Rahmen der GI-Jahrestagung 1997. Verlag der Augustinus Buchhandlung (Aachener Beiträge zur Informatik, Band 21), Otto Spaniol (Hrsg.).

Thomas Kolbe and Sabine Glesner (1997). Many-Sorted Logic in a Learning Theorem Prover. Proceedings of the 21st German Annual Conference on Artificial Intelligence (KI'97). Springer Verlag, Lecture Notes in Computer Science, 75-86.

Sabine Glesner (1998). Many-Sorted Natural Semantics - Specification and Generation of the Semantic Analysis for Imperative and Object-Oriented Programming Languages. Proceedings of the Workshop on Functional and Logic Programming

Sabine Glesner and Wolf Zimmermann (1998). Using Many-Sorted Natural Semantics to Specify and Generate Semantic Analysis. Proceedings of the Systems Implementation Conference (SI2000). Chapman & Hall, 249-262.

Sabine Glesner and Karl Stroetmann (1999). Combining Inclusion Polymorphism and Parametric Polymorphism. Computing Research Repository: Logic in Computer Science Document ID: xxx.cs.LO/9906013, NCSTRL-Server http://www.ncstrl.org/.

Sabine Glesner (1999). Natürliche Semantik für imperative und objektorientierte Programmiersprachen. Shaker Verlag.

Sabine Glesner (1999). Natural Semantics for Imperative and Object-Oriented Programming Languages. Proceedings der 29. Jahrestagung der Gesellschaft für Informatik, Arbeitstagung Programmiersprachen. Springer Verlag, 370-379.

Sabine Glesner and Wolf Zimmermann (2001). Structural Simulation Proofs based on ASMs even for Non-Terminating Programs. Proceedings of the ASM-Workshop, Eight International Conference on Computer Aided Systems Theory EUROCAST 2001, 235-238.

Sabine Glesner and Rubino Geiß and Boris Boesler (2002). Verified Code Generation for Embedded Systems. In Proceedings of the COCV-Workshop 2002 (Compiler Optimization meets Compiler Verification). 5th European Conferences on Theory and Practice of Software (ETAPS 2002), 1-18.

Jan Olaf Blech (2003). Spezifikation und maschinelle Verifikation von Konstantenfaltung in Übersetzern.

Sabine Glesner (2003). Using Program Checking to Ensure the Correctness of Compiler Implementations. Journal of Universal Computer Science (J.UCS), 191-222.

Sabine Glesner (2003). ASMs versus Natural Semantics: A Comparison with New Insights. Abstract State Machines - Advances in Theory and Applications, Proceedings of the 10th International Workshop, ASM 2003. Springer Verlag, Lecture Notes in Computer Science, Vol. 2589, 293-308.

Sabine Glesner and Jan Olaf Blech (2003). Classifying and Formally Verifying Integer Constant Folding. Proceedings of the Workshop COCV 2003: Compiler Optimization meets Compiler Verification. Electronic Notes in Theoretical Computer Science (ENTCS), Vol. 82, No. 2.

Sabine Glesner (2003). Program Checking with Certificates: Separating Correctness-Critical Code. Proceedings of the 12th International FME Symposium (Formal Methods Europe). Springer Verlag, Lecture Notes in Computer Science, Vol. 2805, 758-777.

Jan Olaf Blech (2004). Eine formale Semantik für SSA-Zwischensprachen in Isabelle/HOL.

Sabine Glesner and Simone Forster and Matthias Jäger (2004). A Program Result Checker for the Lexical Analysis of the GNU C Compiler. Proceedings of the COCV-Workshop (Compiler Optimization meets Compiler Verification), 7th European Conferences on Theory and Practice of Software (ETAPS 2004). Elsevier, Electronic Notes in Theoretical Computer Science (ENTCS), 19 - 35.

Sabine Glesner (2004). A Proof Calculus for Natural Semantics Based on Greatest Fixed Point Semantics. Proceedings of the COCV-Workshop (Compiler Optimization meets Compiler Verification), 7th European Conferences on Theory and Practice of Software (ETAPS 2004). Elsevier, Electronic Notes in Theoretical Computer Science (ENTCS), 73 - 93.

Sabine Glesner and Wolf Zimmermann (2004). Natural Semantics as a Static Program Analysis Framework. ACM Transactions on Programming Languages and Systems (TOPLAS), 510-577.

Sabine Glesner and Gerhard Goos and Wolf Zimmermann (2004). Verifix: Konstruktion und Architektur verifizierender Übersetzer (Verifix: Construction and Architecture of Verifying Compilers). it - Information Technology, 265 - 276.

Sabine Glesner (2004). An ASM Semantics for SSA Intermediate Representations. Proceedings of the 11th International Workshop on Abstract State Machines. Springer Verlag, Lecture Notes in Computer Science, 144 - 160.

Sabine Glesner and G. Goos and F. v. Henke and H. Langmaack and W. Goerigk and W. Zimmermann (2004). Abschlussbericht Verifix. Bericht zur Vorlage bei der Deutschen Forschungsgemeinschaft

Jan Olaf Blech and Sabine Glesner (2004). A Formal Correctness Proof for Code Generation from SSA Form in Isabelle/HOL. Proceedings der 3. Arbeitstagung Programmiersprachen (ATPS) auf der 34. Jahrestagung der Gesellschaft für Informatik. Lecture Notes in Informatics, 449 - 458.

Sabine Glesner (2004). Verification of Optimizing Compilers. Fakultät für Informatik, Universität Karlsruhe

Jan Olaf Blech and Lars Gesellensetter and Sabine Glesner (2005). Formal Verification of Dead Code Elimination in Isabelle/HOL. Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods. IEEE Computer Society Press, 200-209.

Sabine Glesner (2005). An Introduction to (Co)Algebras and (Co)Induction and their Application to the Semantics of Programming Languages.

Stefan Kopp and Lars Gesellensetter and Nicole Krämer and Ipke Wachsmuth (2005). A Conversational Agent as Museum Guide - Design and Evaluation of a Real-World Application. The 5th International Working Conference on Intelligent Virtual Agents (IVA. Springer.

Andreas Humbert (2005). Entwurf und Implementierung einer Schnittstelle für SSA-Sprachen.

Sabine Glesner and Jan Olaf Blech (2005). Logische und softwaretechnische Herausforderungen bei der Verifikation optimierender Compiler. Proceedings der Tagung Software Engineering 2005. Lecture Notes in Informatics (LNI), 131-140.

Jan Olaf Blech and Sabine Glesner and Johannes Leitner and Steffen Mülling (2005). Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL. Proceedings of the COCV-Workshop (Compiler Optimization meets Compiler Verification), 8th European Conferences on Theory and Practice of Software (ETAPS 2005). Elsevier, 33-51.

Jan Olaf Blech and Sabine Glesner and Johannes Leitner (2005). Formal Verification of Java Code Generation from UML Models. Proceedings of the 3rd International Fujaba Days 2005, "MDD in Practice". Technical Report, University of Paderborn, 49-56.

Nora Toussaint and Elke Salecker (2005). Gegenbeispielgesteuerte Abstraktionsverfeinerung in High-Level-Petrinetzen.

Sabine Glesner (2005). Optimierende Compiler: Vertrauen ist gut, Verifikation ist besser!.

Sabine Glesner (2006). Efficient Construction and Verification of Embedded Software. Embedded Systems - Modeling, Technology and Applications. Springer Verlag, 21-32.

Sabine Glesner and Jan Olaf Blech (2006). Coalgebraic Semantics for Component Systems. Architecting Systems with Trustworthy Components, Lecture Notes in Computer Science, Vol. 3938. Springer Verlag.

Lars Gesellensetter and Sabine Glesner (2006). Only the best can make it: optimal component selection. Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA). Electronic Notes in Theoretical Computer Science (ENTCS).

Sabine Glesner and Johannes Leitner and Jan Olaf Blech (2006). Coinductive Verification of Program Optimizations using Similarity Relations. Proceedings of the Workshop Compiler Optimizations meets Compiler Verification (COCV 2006). Electronic Notes in Theoretical Computer Science (ENTCS).

Sabine Glesner (2006). Finite Integer Computations: An Algebraic Foundation for Their Correctness. Formal Aspects of Computing,

M. Broy and M. Jarke and M. Nagl and D. Rombach (Redaktion) and A. Cremers and J. Ebert and Sabine Glesner and M. Glinz and M. Goedicke and G. Goos and V. Gruhn and W. Hasselbring and Stefan Jähnichen and S. Kowalewski and B. Krämer and S. Leue and C. Lewerentz and P. Liggesmeyer and C. Lüth and B. Paech and H. Partsch and I. Philippow and L. Prechelt and A. Rausch and w.-P. de Roever and B. Rumpe and G. Rünger and W. Schäfer and K. Schneider and A. Schürr and W. Tichy and B. Westfechtel and W.Zimmermann and A. Zündorf (Mit-Autoren/Unterzeichner) (2006). Dagstuhl-Manifest zur strategischen Bedeutung des Software Engineering in Deutschland. Perspectives Workshop \"Challenges for Software Engineering Research\"

Holger Giese and Sabine Glesner and Johannes Leitner and Wilhelm Schäfer and Robert Wagner (2006). Towards Verified Model to Code Transformations. Proc. of the 3rd Workshop on Model design and Validation (MoDeV2a'06): Perspectives on Integrating MDA and V&V, ACM/IEEE International Conference on Model Driven Engineering Languages and Systems

(2007). Proceedings of the 6th International Workshop on Compiler Optimization meets Compiler Verification, COCV'07. COCV. Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier.

Sabine Glesner (2007). Optimierende Compiler: Vertrauen ist gut, Verifikation ist besser!. Unsere Zukunft 2020 - Was morgen und übermorgen Stand der Technik sein könnte. Universum Verlag.

Sabine Glesner and Stefan Jähnichen and Barbara Paech and Bernhard Rumpe and Thomas Wetter and Alfred Winter (2007). Manifest: Strategische Bedeutung des Software Engineering für die Medizin. Informatik – Forschung und Entwicklung

Sabine Glesner and Steffen Helke and Stefan Jähnichen (2007). VATES: Verifying the Core of a Flying Sensor. Proc. Conquest 2007, 10th International Conference on Quality Engineering in Software Technology. dpunkt Verlag.

Lars Gesellensetter and Sabine Glesner and Elke Salecker (2007). Formal Verification with Isabelle/HOL in Practice: Finding a Bug in the GCC Scheduler. 12th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2007)

Michael Beyer and Andreas Rose and Emanuel Jank and Jörg Krüger (2007). Enhancing instrument support of a power controlling ENT navigation system (FESS-Control). CAS-H '07: Proceedings of the 4th International Computer Aided Surgery Around the Head Conference. Pro Business Verlag, 19–20.

Sabine Glesner and Stefan Jähnichen and Barbara Paech and Bernhard Rumpe and Thomas Wetter and Alfred Winter (2007). Strategische Bedeutung des Software Engineering für die Medizin. Proceedings der Tagung Software Engineering 2007. Lecture Notes in Informatics (LNI).

Sabine Glesner and Andreas Humbert (2008). A Formal Semantics of Intermediate Compiler Representations in Isabelle/HOL. Proceedings of the Workshop Compiler Optimization meets Compiler Verification (COCV 2008). Elsevier.

Dirk Tetzlaff (2008). Erweitertes Hyperblock-Scheduling für VLIW-Prozessoren. GI Informatiktage 2008. Köllen Druck+Verlag GmbH, 111-114.

Lars Gesellensetter and Sabine Glesner (2008). Interprocedural Speculative Optimization of Memory Accesses to Global Variables. European Conference on Parallel and Distributed Computing (Euro-Par 2008). LNCS.