CSL862 : Compiler/OS Design and Verification

Sem I, 2014-15

Links to notes etc. on future days are tentative only. They are here only to give you an idea what the future will bring. The lectures will be organized as discussions, so it is very important that you read the paper before the class (see PREP). Homeworks need to be submitted at the start of the respective lectures.
MondayTuesdayWednesdayThursdayFriday
Jul 21Jul 22
Introduction
Jul 23
High-level discussion on Compiler Design
Jul 24
Jul 25
Symbolic Execution for Straight-Line Code
Jul 28
Jul 29
Id-ul-Fitr
Jul 30
Symbolic Execution for Code with Branches. Introductory discussion on Undecidability of Program Equivalence.
Jul 31
Aug 1
No Lecture
Aug 4
Aug 5
Simulation Relation. Work through loop peeling example
Aug 6
Programming Assignment Session
Aug 7
Aug 8
Undecidability of Halting Problem, Program Equivalence
Aug 11
Aug 12
Aditya Kanade's talk
Aug 13
Programming Assignment
Aug 14
Aug 15
Independence Day
Aug 18
Aug 19
Translation Validation
PREP: read paper, example
Aug 20
Translation Validation contd.
Aug 21
Aug 22
Programming Assignment
Aug 25
Aug 26
Translation Validation contd.
Aug 27
Translation Validation wrap-up (HW2 due)
Aug 28
Aug 29
Minor1 Tests
Sep 1
Sep 2
Proof-Carrying Code
PREP: read paper
Sep 3
Proof-Carrying Code contd.
Sep 4
Sep 5
Programming Assignment
Sep 8
Sep 9
Proof-Carrying Code contd.
PREP: read paper
Sep 10
Discussion on Lab2
Sep 11
Sep 12
Typed Assembly Language
PREP: read paper
Sep 15
Sep 16
Typed Assembly Language (..contd.)
Sep 17
Typed Assembly Language (code preconditions)
Sep 18
Sep 19
Typed Assembly Language (static data types, macro instructions)
Sep 22
Sep 23
Midterm Test
Sep 24
Talk by Puneet on Finagle @ Twitter
Sep 25
Sep 26
Typed Assembly Language (function and stack types)
Sep 29
Sep 30
Typed Assembly Language (malloc, limits of our type system)
Oct 1
Typed Assembly Language (array types, type encodes array length)
Oct 2
Oct 3
Dusshera
Oct 6
Oct 7
Typed Assembly Language (ADTs. e.g., list. Dependent Types: Odd/Even, Static length lists)
Oct 8
Minor2 Tests
Oct 9
Oct 10
Minor2 Tests
Oct 13
Oct 14
Dependently Typed Assembly Language
PREP: read paper
Oct 15
Operational Semantics
Oct 16
Oct 17
Type-Checking
Oct 20
Oct 21
Mid-sem break
Oct 22
Mid-sem break
Oct 23
Oct 24
Mid-sem break
Oct 27
Oct 28
Type-Inference
Oct 29
Reading break
Oct 30
Oct 31
Parameterized Program Equivalence Checker
PREP: read paper
Nov 3
Nov 4
Muharram
Nov 5
PEC paper contd.
Nov 6
Nov 7
Thursday timetable
Nov 10
Nov 11
No classes due to placement
Nov 12
Translation Validation with Meta-variables. Software Pipelining Example
Nov 13
Nov 14
Compiler Optimizations (Friday and Saturday lecture)
Nov 17
Nov 18
Compcert
PREP: read Compcert Manual Chapter 1, paper
Nov 19
Compcert contd.
PREP: notes based on this tutorial. Example src file
Nov 20
Nov 21
Compcert contd.