Compiler Verification Seminar
People
The seminar won the teaching award in the category Seminar.
Organization
| 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.
Dates
The preparatory meeting was held on October 24, 11:45 am in Room 401 in E 1.3.
Sessions
| 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 |
Talks
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.
Topics
Introduction
| [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 ] |
CompCert
[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 ] |