Compiler Verification Seminar
|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|
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.
|November 7||Sigurd Schneider||Please read [M1,M2] as introduction to the topic.|
|November 14||David Pfaff||||April 19, 9:00|
|November 21||Hazem Torfah||||April 19, 10:00|
|November 28||Johannes Doerfert||. You might want to look at [S3] to know more about equality saturation.||April 19, 11:00|
|December 5||Tim Ruffing||||April 19, 14:00|
|December 19||Tobias Tebbi||||April 19, 15:00|
|January 9||Sebastian Hahn||||April 20, 10:00|
|January 16||Carsten Hornung||||April 20, 11:00|
|January 23||Steven Schäfer||||April 20, 12:00|
|January 30||Bernhard Schommer||||April 20, 14:00|
|February 6||Jonas Kaiser||||April 20, 15:00|
|[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 ]|
|||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 ]|
|||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 ]|
|||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 ]|
|||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 ]|
|||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 ]|
 will be assigned to a team of 3 students.
|||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 ]|
|||Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363-446, 2009. [ .pdf ]|
Compositional Compiler Correctness
|||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 ]|