CSL862: Spl. Topics in Software Systems: Compiler/OS Design and Verification
Sem I, 2014-15
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.
will be required to read the papers before the class (see schedule). Exams will be open book, open notes.
- Jul 30 Translation Validation paper posted on schedule page.
- End of course: Course feedback posted.
- Introduction to Symbolic Execution : Checking Semantics of Acyclic Programs (submission instructions)
- Translation Validation Implementation
- Homework on Simulation Relations
- Homework on Translation Validation