Seminar Compilerbau und Verifikation

SE 12077

Seminar Compilerbau und Verifikation

Prof. Dr. R. Loogen, Prof. Dr. H.P. Gumm, Dipl. Inform. Jost Berthold

Termin: Mi, 16.15 - 18 Uhr, SR V, Lahnberge, Ebene D5

Vorbesprechung mit Themenvergabe: Mi 22.02.2006, 10:00 - 10.45 Uhr, SR V, Lahnberge, Ebene D5
Es sind noch Themen zu vergeben. Bitte wenden Sie sich bei Interesse an die Organisatoren.
Beginn: 10. Mai 2006
Achtung: Am 14. Juni und am 28. Juni, dem Sport-Dies, findet kein Seminarvortrag statt.

Fachgebiet	Klassifikation	Semester	Fortsetzung	Skript
Informatik	Hauptstudium	>=5	-	nein

Voraussetzungen: Grundkenntnisse im Compilerbau, wie sie in Vorlesung im Wintersemester 2005/06 vermittelt wurden.

Lernziele:

Vertiefung von Kenntnissen in den Bereichen Compilerbau und Verifikation
Erwerb von Fähigkeiten und Techniken des wissenschaftlichen Arbeitens;
Erwerb von Fähigkeiten und Fertigkeiten beim Lesen und Reproduzieren/Zusammenfassen wissenschaftlicher Texte;
Ausbau von Fähigkeiten der mündlichen Präsentation wissenschaftlicher Abhandlungen in Form eines Vortrags und durch die aktive Teilnahme an der Diskussion zu anderen Vorträgen

Scheinkriterien: schriftliche Ausarbeitung und Vortrag eines ausgewählten Themas, regelmäßige Teilnahme am Seminar
Merkblatt zur Ausarbeitung und zum Vortrag (pdf, ps)

Inhalt: Es werden neuere Arbeiten aus den Gebieten Compilerbau und Verifikation vorgestellt und diskutiert.

Themen:

Tools
1. Gregor Bonifer: Parsec - eine monadische Parserkombinatoren-Bibliothek für Haskell
  Termin: 10. Mai 2006
  - Parsec-Website
  - Daan Leijen, Erik Meijer: Parsec: Direct Style Monadic Parser Combinators for The Real World, Technical Report UU-CS-2001-35, Departement of Computer Science, Universiteit Utrecht, 2001.
2. Steffen Springer: UUAG - Das Utrecht Attribute Grammar System
  Termin: 24. Mai 2006
  - UUAG Website
  - Wouter Swierstra: Why Attribute Grammars Matter, Article for the Monad.Reader, 01-07-2005 (Original-Link).
  - S. Doaitse Swierstra, Pablo R. Azero Alcocer, Joao Saraiva: Designing and Implementing Combinator Languages, Third School on Advanced Functional Programming 1998.
3. Christina Heitzer: HappyGLR - Erweiterung von Happy zur Behandlung mehrdeutiger Grammatiken
  Termin: 31. Mai 2006
  - HappyGLR Website
  - Paul Callaghan: Ambiguous Parsing With Happy, Eingereicht bei Journal of Functional Programming, Aug. 2005.
Verifikation von OO-Programmen
1. Martin Schwarz: Verifikation rekursiver Prozeduren
  Termin: 7. Juni 2006
  - Th. Kleymann: Hoare Logic and Auxiliary Variables, Internal Report, University of Edinburgh 1998.
Compiler-Backend
1. Andreas Schöneck: Zwischensprachen
  Termin: 21. Juni 2006
  - Stephen Muchnick: Intermediate Representations, Chapter 4 in Abvanced Compiler Design and Implementation, Morgan Kaufmann Publishers 1997.
  - Keith D. Cooper and Linda Torcson: Intermediate Representations, Chapter 5 in Engineering a Compiler, Morgan Kaufmann Publishers 2004.
  - .Net-Technologie: MSIL und MSIL Disassembler
2. Marco Kurzrock: Registerallokation
  Termin: 5. Juli 2006
  - Keith D. Cooper and Linda Torcson: Register Allocation, Chapter 12 in Engineering a Compiler, Morgan Kaufmann Publishers 2004.
3. M. Touhafi: Bäume: Mustererkennung und Analyse
  Termin: 12. Juli 2006 - Achtung: Der Vortrag entfällt!
  - R. Wilhelm, D. Maurer: Übersetzerbau, Springer Verlag 1992, Kapitel 10.
Typbasierte Programmanalyse
1. Anastasiya Nonenmacher: Das MRG (Mobile Resource Guarantees)-Projekt
  Termin: 19. Juli 2006
  - MRG Website
  - David Aspinall, Stephen Gilmore, Martin Hofmann, Donald Sannella, Ian Stark: Mobile Resource Guarantees for Smart Devices, In Construction and Analysis of Safe, Secure, and Interoperable Smart Devices: Proceedings of the International Workshop CASSIS 2004, Springer-Verlag, 2005, No. 3362, pages 1-26.
  - M. Hofmann and S. Jost. Static Prediction of Heap Space Usage for First-Order Functional Programs. In POPL’03 — Symposium on Principles of Programming Languages, pages 185–197, New Orleans, LA, USA, January 2003. ACM Press.
  - S. Gilmore and M. Prowse. Proof-carrying bytecode. In Proceedings of First Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE '05), Edinburgh, Scotland, April 2005.
  - Donald Sannella, Martin Hofmann et al.: Mobile Resource Guarantees Evaluation Paper, Trends in Functional Programming 2005.

Noch zu vergebende Themen:

Compiler Tools
1. Frown - ein LALR(k) Parsergenerator für Haskell
  - Frown-Website
  - Ralf Hinze, Ross Patterson: Derivation of a Typed Functional LR Parser, Internal Report 2005.
Proof Carrying Code (PCC)
1. Einführung in Proof Carrying Code
  - George Necula's Proof Carrying Code Website
  - George C. Necula. Proof-Carrying Code. ACM Conference on Principles of Programming Languages (POPL 97), January 1997.
  - Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Ken Cline, Mark Plesko. A Certifying Compiler for Java. In Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI00), Vancouver, British Columbia, Canada, June 18-21, 2000.
2. Spezifikation von Security Policies
  - D Walker: Security Automata
3. Authentifizierungsprotokolle mit PCC
  - A. Appel, E. Felten: Proof Carrying Authentification
Verifikation von OO-Programmen
1. F. deBoer, C. Pierik: Syntax directed Programming Logic for Object Oriented Programming Concepts
2. F. deBoer, C. Pierik: How to cook a complete Hoare Logic for your Pet OO-Language
3. A. Zeller: Isolating Cause Effect Chains from Computer Programs
Typbasierte Programmanalyse
1. TyPiCal - a type-based static analyzer for the pi-calculus
  - TyPiCal - Website
  - Naoki Kobayashi, Type Systems for Concurrent Programs, Proceedings of UNU/IIST 10th Anniversary Colloquium Springer LNCS 2757, pp.439-453
  - Naoki Kobayashi, Type-Based Information Flow Analysis for the Pi-Calculus, Acta Informatica, 42(4-5), pp.291-347, 2005.
Compiler Backend
1. Instruction Scheduling
  - Keith D. Cooper and Linda Torcson: Instruction Scheduling, Chapter 11 in Engineering a Compiler, Morgan Kaufmann Publishers 2004.

Zuletzt geändert:

Voraussetzungen:	Grundkenntnisse im Compilerbau, wie sie in Vorlesung im Wintersemester 2005/06 vermittelt wurden.
Lernziele:	Vertiefung von Kenntnissen in den Bereichen Compilerbau und Verifikation Erwerb von Fähigkeiten und Techniken des wissenschaftlichen Arbeitens; Erwerb von Fähigkeiten und Fertigkeiten beim Lesen und Reproduzieren/Zusammenfassen wissenschaftlicher Texte; Ausbau von Fähigkeiten der mündlichen Präsentation wissenschaftlicher Abhandlungen in Form eines Vortrags und durch die aktive Teilnahme an der Diskussion zu anderen Vorträgen
Scheinkriterien:	schriftliche Ausarbeitung und Vortrag eines ausgewählten Themas, regelmäßige Teilnahme am Seminar Merkblatt zur Ausarbeitung und zum Vortrag (pdf, ps)
Inhalt:	Es werden neuere Arbeiten aus den Gebieten Compilerbau und Verifikation vorgestellt und diskutiert.