Compiler Verification Seminar


Sebastian Hack, Sigurd Schneider

The seminar won the teaching award in the category Seminar.


Language English
Participants 10
Preparatory Meeting October 24 11:45 am , Rm. 401 in E 1.3
Weekly Meeting Monday 16:15, Rm. 401 in E 1.3
starting November 7
Availability Already fully booked

Modus Operandi

There are mandatory papers (index starting with 'M') and presentation papers (numbers 1-8). Each presentation paper below will be assigned to one or more participant(s).

There will be a weekly meeting to discuss each of the mandatory and presentation papers. For each of these meetings, every participant will submit a short summary of the discussed paper(s). Please write 450 words and submit to Sigurd (preferably via email). Summaries are due every Friday before the next meeting at noon. I will make the summaries available by Friday night.

At the end of the semester every participant will give a presentation about her/his paper.


The preparatory meeting was held on October 24, 11:45 am in Room 401 in E 1.3.


Date Discussion Notes Talk
November 7 Sigurd Schneider Please read [M1,M2] as introduction to the topic.
November 14 David Pfaff [1] April 19, 9:00
November 21 Hazem Torfah [2] April 19, 10:00
November 28 Johannes Doerfert [3]. You might want to look at [S3] to know more about equality saturation. April 19, 11:00
December 5 Tim Ruffing [4] April 19, 14:00
December 12 Excursion
December 19 Tobias Tebbi [5] April 19, 15:00
January 9 Sebastian Hahn [6] April 20, 10:00
January 16 Carsten Hornung [7] April 20, 11:00
January 23 Steven Schäfer [7] April 20, 12:00
January 30 Bernhard Schommer [7] April 20, 14:00
February 6 Jonas Kaiser [8] April 20, 15:00


The talks will take place April 19, from 9:00 - 12:00 and 14:00 - 16:00, and April 20 10:00-13:00 and 14:00-16:00 in Room 401.



[M1] John McCarthy and James Painter. Correctness Of A Compiler For Arithmetic Expressions. 1967. [ .pdf ]
[M2] Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107-115, 2009. [ .pdf ]

Translation Validation

[1] Amir Pnueli, Michael Siegel, and Eli Singerman. Translation validation. In Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, pages 151-166, London, UK, 1998. Springer-Verlag. [ .ps ]
[2] George C. Necula. Translation validation for an optimizing compiler. In Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, PLDI '00, pages 83-94. ACM, 2000. [ .pdf  ]
[3] Michael Stepp, Ross Tate, and Sorin Lerner. Equality-based translation validator for LLVM. In Proceedings of the 23th International Conference on Computer Aided Verification, CAV 2011, vol. 6806 of Lecture Nodes in Computer Science, pages 737-742. Springer, 2011. [ .pdf ]
[S3] Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. Equality Saturation: A New Approach to Optimization. In Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, POPL 2009, pages 264-276. ACM, 2009. [ .pdf ]

Proof-carrying Code and Typed Assembly Language

[M3] is a mandatory read and will not be presented.

[M3] G. Necula and P. Lee. Research on proof-carrying code for untrusted-code security. In Proceedings of the 1997 IEEE Symposium on Security and Privacy, SP '97, page 204, Washington, DC, USA, 1997. IEEE Computer Society. [ .ps ]
[4] George C. Necula. Proof-carrying code. In Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '98, pages 85-97. ACM, 1998. [ .ps ]
[5] Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From system F to typed assembly language. In Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '97, pages 106-119. ACM, 1997. [ .pdf ]


[7] will be assigned to a team of 3 students.

[6] Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy. Formal verification of a C compiler front-end. In FM 2006: Int. Symp. on Formal Methods, volume 4085 of Lecture Notes in Computer Science, pages 460-475. Springer, 2006. [ .pdf ]
[7] Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363-446, 2009. [ .pdf ]

Compositional Compiler Correctness

[8] Chung-Kil Hur and Derek Dreyer. A Kripke logical relation between ML and assembly. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of programming languages, POPL '11. ACM, 2011. [ .pdf ]