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

Sem I, 2014-15


Home   –   Administrivia   –   Schedule

Intro

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.

News

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

Homeworks

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