	Veröffentlichungen

Forschungsgebiete

Veröffentlichungen

Forschungskolloquium

Aktuelle Veranstaltungen

Frühere Veranstaltungen

Aktuelle Informationen

Compilerbau-Projekt
WS2008/09! >>

Alle Veröffentlichungen

2009

Konferenzartikel
Alvincz, Glesner, Breaking the Curse of Static Analyses: Making Compiler Intelligent via Machine Learning. 3rd Workshop on Statistical and Machine learning approaches to ARchitectures and compilaTion (SMART'09)
Herber, Friedemann, Glesner, Combining Model Checking and Testing in a Continuous HW/SW Co-Verification Process. 3rd International Conference on Tests and Proofs (TAP'09)
Göthel, Glesner, Machine Checkable Timed CSP. Proc. of The First NASA Formal Methods Symposium (NFM '09)

2008

Zeitschriftenartikel
Beyer, Rose, Jank, Krüger, Softwaretechnische Instrumentenunterstützung für ein leistungssteuerndes HNO Navigationssystem. Computer Science - Research and Development
Konferenzartikel
Glesner, Humbert, A Formal Semantics of Intermediate Compiler Representations in Isabelle/HOL. 11th European Conferences on Theory and Practice of Software (ETAPS 2008)
Tetzlaff, Erweitertes Hyperblock-Scheduling für VLIW-Prozessoren. GI Informatiktage 2008
Gesellensetter, Glesner, Interprocedural Speculative Optimization of Memory Accesses to Global Variables. European Conference on Parallel and Distributed Computing (Euro-Par 2008)
Herber, Fellmuth, Glesner, Model Checking SystemC Designs Using Timed Automata. 6th International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS 2008)
Hundt, Glesner, Optimizing Aspectual Execution Mechanisms for Embedded Applications. 11th European Conferences on Theory and Practice of Software (ETAPS 2008)
Technischer Bericht
Gesellensetter, Scalable Analysis via Machine Learning: Predicting Memory Dependencies Precisely. Dagstuhl Seminar Proceedings 08161
Poster
Tetzlaff, Erweitertes Hyperblock-Scheduling für VLIW-Prozessoren. GI Informatiktage 2008

2007

Konferenzband
Sabine Glesner, Jens Knoop, Rolf Drechsler (ed.), Proceedings of the 6th International Workshop on Compiler Optimization meets Compiler Verification, COCV'07. COCV
Buchkapitel
Glesner, Optimierende Compiler: Vertrauen ist gut, Verifikation ist besser!. Unsere Zukunft 2020 - Was morgen und übermorgen Stand der Technik sein könnte
Zeitschriftenartikel
Glesner, Jähnichen, Paech, Rumpe, Wetter, Winter, Manifest: Strategische Bedeutung des Software Engineering für die Medizin. Informatik -- Forschung und Entwicklung
Eingeladene Papiere
Glesner, Jähnichen, Paech, Rumpe, Wetter, Winter, Strategische Bedeutung des Software Engineering für die Medizin. Proceedings der Tagung Software Engineering 2007
Glesner, Helke, Jähnichen, VATES: Verifying the Core of a Flying Sensor. Proc. Conquest 2007, 10th International Conference on Quality Engineering in Software Technology
Konferenzartikel
Gesellensetter, Glesner, Salecker, 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)

Diplomarbeit
Tetzlaff, Erweitertes Hyperblock-Scheduling für VLIW-Prozessoren. Technische Universität Berlin, FG PES
Göthel, Formalisierung von Timed CSP im Theorembeweiser Isabelle/HOL. Technische Universität Berlin, FG PES
Schulz, Spekulative Optimierung von Speicherzugriffen in Compilern. Technische Universität Berlin, FG PES

2006

Buchkapitel (collection)
Glesner, Efficient Construction and Verification of Embedded Software. Embedded Systems - Modeling, Technology and Applications
Zeitschriftenartikel
Glesner, Finite Integer Computations: An Algebraic Foundation for Their Correctness. Formal Aspects of Computing,
Konferenzartikel
Glesner, Blech, Coalgebraic Semantics for Component Systems. Architecting Systems with Trustworthy Components, Lecture Notes in Computer Science, Vol. 3938
Glesner, Leitner, Blech, Coinductive Verification of Program Optimizations using Similarity Relations. Proceedings of the Workshop Compiler Optimizations meets Compiler Verification (COCV 2006)
Gesellensetter, Glesner, Only the best can make it: optimal component selection. Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA)
Giese, Glesner, Leitner, Schäfer, Wagner, 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
Technischer Bericht
Broy, Jarke, Nagl, (Redaktion), Cremers, Ebert, Glesner et.al., Dagstuhl-Manifest zur strategischen Bedeutung des Software Engineering in Deutschland. Perspectives Workshop \"Challenges for Software Engineering Research\"

Diplomarbeit
Beyer, Entwurf, Realisierung und Integration einer dynamischen Instrumentenmodellierung für ein klinisches Navigationssystem mit Leistungssteuerung für die HNO-Chirurgie. BZMM - Berliner Zentrum für Mechatronische Medizintechnik
Humbert, Formalisierung einer Strukturell Operationalen Semantik für eine SSA-Zwischensprache im Theorembeweiser Isabelle/HOL. Technische Universität Berlin, FG PES
Leitner, Verifikation von Modelltransformationen basierend auf Triple Graph Grammatiken. Technische Universität Berlin, FG PES

2005

Konferenzartikel
Kopp, Gesellensetter, Krämer, Wachsmuth, A Conversational Agent as Museum Guide - Design and Evaluation of a Real-World Application. The 5th International Working Conference on Intelligent Virtual Agents (IVA
Blech, Gesellensetter, Glesner, Formal Verification of Dead Code Elimination in Isabelle/HOL. Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods
Blech, Glesner, Leitner, Formal Verification of Java Code Generation from UML Models. Proceedings of the 3rd International Fujaba Days 2005, "MDD in Practice"
Glesner, Blech, Logische und softwaretechnische Herausforderungen bei der Verifikation optimierender Compiler. Proceedings der Tagung Software Engineering 2005
Blech, Glesner, Leitner, Mülling, Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL. Electronic Notes in Theoretical Computer Science (ENTCS)
Technischer Bericht
Glesner, An Introduction to (Co)Algebras and (Co)Induction and their Application to the Semantics of Programming Languages. Fakultät für Informatik, Universität Karlsruhe
Glesner, Optimierende Compiler: Vertrauen ist gut, Verifikation ist besser!. Fakultät für Informatik, Universität Karlsruhe

Diplomarbeit
Toussaint, Salecker, Gegenbeispielgesteuerte Abstraktionsverfeinerung in High-Level-Petrinetzen. Humboldt-Universität zu Berlin
Studienarbeit
Leitner, Coalgebraic Methods in Verification of optimizing Program transformations using Theorem provers. Universität Karlsruhe
Humbert, Entwurf und Implementierung einer Schnittstelle für SSA-Sprachen. Universität Karlsruhe

2004

Zeitschriftenartikel
Glesner, Zimmermann, Natural Semantics as a Static Program Analysis Framework. ACM Transactions on Programming Languages and Systems (TOPLAS)
Glesner, Goos, Zimmermann, Verifix: Konstruktion und Architektur verifizierender Übersetzer (Verifix: Construction and Architecture of Verifying Compilers). it - Information Technology
Konferenzartikel
Blech, Glesner, 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
Glesner, Forster, Jäger, 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)
Glesner, 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)
Glesner, An ASM Semantics for SSA Intermediate Representations. Proceedings of the 11th International Workshop on Abstract State Machines
Technischer Bericht
Glesner, Goos, Henke, Langmaack, Goerigk, Zimmermann, Abschlussbericht Verifix. Bericht zur Vorlage bei der Deutschen Forschungsgemeinschaft

Habilitation
Glesner, Verification of Optimizing Compilers. Fakultät für Informatik, Universität Karlsruhe
Diplomarbeit
Blech, Eine formale Semantik für SSA-Zwischensprachen in Isabelle/HOL . Universität Karlsruhe, Fakultät für Informatik

2003

Zeitschriftenartikel
Glesner, Using Program Checking to Ensure the Correctness of Compiler Implementations . Journal of Universal Computer Science (J.UCS)
Konferenzartikel
Glesner, 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
Glesner, Blech, Classifying and Formally Verifying Integer Constant Folding. Proceedings of the Workshop COCV 2003: Compiler Optimization meets Compiler Verification
Glesner, Program Checking with Certificates: Separating Correctness-Critical Code. Proceedings of the 12th International FME Symposium (Formal Methods Europe)

Studienarbeit
Blech, Spezifikation und maschinelle Verifikation von Konstantenfaltung in Übersetzern. Universität Karlsruhe, Institut für Programmstrukturen und Datenorganisation

2002

Konferenzartikel
Glesner, Geiß, Boesler, Verified Code Generation for Embedded Systems. In Proceedings of the COCV-Workshop 2002 (Compiler Optimization meets Compiler Verification)

2001

Konferenzartikel
Glesner, Zimmermann, 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

1999

Konferenzartikel
Glesner, Natural Semantics for Imperative and Object-Oriented Programming Languages. Proceedings der 29. Jahrestagung der Gesellschaft für Informatik, Arbeitstagung Programmiersprachen
Technischer Bericht
Glesner, Stroetmann, 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/

Dissertation
Glesner, Natürliche Semantik für imperative und objektorientierte Programmiersprachen. Universität Karlsruhe

1998

Konferenzartikel
Glesner, 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
Glesner, Zimmermann, Using Many-Sorted Natural Semantics to Specify and Generate Semantic Analysis. Proceedings of the Systems Implementation Conference (SI2000)

1997

Konferenzartikel
Kolbe, Glesner, Many-Sorted Logic in a Learning Theorem Prover. Proceedings of the 21st German Annual Conference on Artificial Intelligence (KI'97)
Glesner, Zimmermann, 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

1996

Diplomarbeit
Glesner, Mehrsortige Logik in einem Lernenden Beweiser. Technische Hochschule Darmstadt, Fachbereich Informatik

1995

Konferenzartikel
Glesner, Koller, 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

1994

Master's Thesis
Glesner, Constructing Flexible Dynamic Belief Networks from First-Order Probabilistic Knowledge Bases. University of California, Berkeley, Department of Electrical Engineering and Computer Science


	PES-Web [ 10.03.2010. 14:46:28 ] — Based on ITM-Web/IpdWeb developed 2002-2005 @ Ipd-Goos & Ipd-Tichy & ITM-Zitterbart