Vorlesung Gliederung Kommentar Übungen Univis  

Probleme beim Bau voll korrekter Übersetzer, WS 2004 / 05 (080085)

Vorlesung, 4 SWS, Schein, ECTS-Studium, ECTS-Credits: 4,0, Fachgebiet: Praktische Informatik
Zeit und Ort: Di, Mi 16 - 18 c.t., Raum wird noch bekanntgegeben
Erster Termin: Di 19. 10. 2004

Dozent
PD Dr. Wolfgang Goerigk

Verweise
Übungen zur Vorlesung Probleme beim Bau voll korrekter Übersetzer

Gliederung

Kommentar

Empfohlene Literatur
Aho, Ullman: The Theory of Parsing, Translation and Compiling I, II. Prentice-Hall, 1973.
Gries: Compiler Construction for Digital Computers. Wiley, 1971.
Alagic, Arbib: The Design of Well Structured and Correct Programs. Springer, 1978.
Moore: Piton. A Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers, 1996.
Allan: The Anatomy of Lisp.
Loeckx, Sieber: The Foundations of Program Verification. Wiley-Teubner, 1984.
Müller-Olm: Modular Compiler Verification. Springer LNCS 1283, 1997

Einige der Vorlesung zugrundeliegende Artikel:

Compiler Verification Revisited. Computer Aided Reasoning, ACL2 Case Studies. Kluwer, 2000.
Proving Preservation of Partial Correctness with ACL2: A Mechanical Compiler Source Level Correctness Proof. ACL2 Workshop 2000, Austin, Texas.
mit H. Langmaack: Realistic Correct Systems Implementation. Int. Journal on Problems in Programming (1), 2003.
mit H. Langmaack: Trusted Compiler Implementation. Int. Journal on Problems in Programming (2), 2003.

Auf weitere Literatur wird jeweils in der Vorlesung hingewiesen.