CSL862: Spl. Topics in Software Systems: Compiler/OS Design and Verification

Sem I, 2014-15

Home   –   Administrivia   –   Schedule


This course will discuss verification techniques for the compiler and OS. We will look at static analysis techniques, including symbolic execution, translation validation, proof-carrying code, program types, and verified compiler design.

The course will involve programming assignments, and one lecture per week will be dedicated only for programming assignment-related issues.

This course will be organized as a paper reading course. You will be required to read the papers before the class (see schedule). Exams will be open book, open notes.


Programming Assignments

  1. End of course: Course feedback posted.
  2. Introduction to Symbolic Execution : Checking Semantics of Acyclic Programs (submission instructions)
  3. Translation Validation Implementation


  1. Homework on Simulation Relations
  2. Homework on Translation Validation