plt17:top

**Instructor:** Hossein Hojjat

**Email:** hh at cs rit edu

** Office hours (GOL-3545):**

- Tu 11am – 12am
- Th 11am - 12am

**Lectures:** MoWeFr 1:25PM - 2:20PM (GOL-1445)

**Final Exam:**
12/18/2017 (12:30 PM - 2:30 PM) ,
Place: GOL-1445

**Description & Policies:**

CS Common Course Policies

Grading Policies

Homework Assignment Policies

**Acknowledgements:**

Portions of this course material based upon similar courses offered by Armando Solar-Lezama and Adam Chlipala.

**Recommended Books:**

Monday 08/28 | Lecture 1: Course Overview | Slides |

Wednesday 08/30 | Lecture 2: Introduction to Scala | Slides |

Friday 09/01 | Lecture 3: Functions in Scala | Slides |

Monday 09/04 | Labor Day | |

Wednesday 09/06 | Lecture 4: Types in Scala | Slides |

Friday 09/08 | Lecture 5: Boolean Satisfiability (SAT) Solving | Slides |

Monday 09/11 | Lecture 6: The λ-calculus | Slides |

Wednesday 09/13 | Instructor attending RV 2017 | |

Friday 09/15 | Lecture 7: Programming in the λ-calculus | Slides |

Monday 09/18 | Lecture 8: The λ-calculus Semantics | Slides |

Wednesday 09/20 | Lecture 9: Introduction to Coq | Slides |

Friday 09/22 | Lecture 10: Coq Demo |

Monday 09/25 | Lecture 11: Introduction to Simple Types | Slides |

Wednesday 09/27 | Lecture 12: Simple Types: Progress & Preservation | Slides |

Friday 09/29 | Lecture 13: Type Inference & Polymorphism | Slides |

Monday 10/02 | Lecture 14: Hindley-Milner Type System | Slides |

Wednesday 10/04 | Lecture 15: Subtyping | Slides |

Friday 10/06 | Lecture 16: Semantics for Imperative Programs | Slides |

Monday 10/09 | October Break | |

Wednesday 10/11 | Lecture 17: Types for Imperative Features | Slides |

Friday 10/13 | Lecture 18: Types for Information Flow | Slides |

Monday 10/16 | Recitation - Assignment 2 Discussion | |

Wednesday 10/18 | Lecture 19: Introduction to Axiomatic Semantics | Slides |

Friday 10/20 | Lecture 20: Hoare Rules | Slides |

Monday 10/23 | Lecture 21: Verification Condition Generation (I) | Slides |

Wednesday 10/25 | Lecture 22: Verification Condition Generation (II) | Slides |

Friday 10/27 | Lecture 23: Verification by Solving Horn Clauses | Slides |

Monday 10/30 | Lecture 24: Verifying Programs with Arrays | Slides |

Wednesday 11/01 | Lecture 25: Verifying Programs with Dynamic Allocation | Slides |

Friday 11/03 | Lecture 26: Hoare Logic for Concurrent Programs | Slides |

Monday 11/06 | Lecture 27: Introduction to Abstract Interpretation | Slides |

Wednesday 11/08 | Lecture 28: Gallois Connection | Slides |

Friday 11/10 | Lecture 29: Collecting Semantics | Slides |

Monday 11/13 | Lecture 30: Widening and Narrowing | Slides |

Wednesday 11/15 | Lecture 31: Introduction to Models and Properties | Slides |

Friday 11/17 | Lecture 32: Temporal Logic | Slides |

Monday 11/20 | Lecture 33: Automata Theoretic Model Checking | Slides |

Wednesday 11/22 | Thanksgiving Break | |

Friday 11/24 | Thanksgiving Break |

Monday 11/27 | Lecture 34: Partial Order Reduction | Slides |

Wednesday 11/29 | Lecture 35: Bounded Model Checking | Slides |

Friday 12/01 | Lecture 36: Software Model Checking | Slides |

Monday 12/04 | Software Synthesis for Networks |

Wednesday 12/06 | Final Presentation: Quinn,Kyle,Bhavin,Joshua |

Friday 12/08 | Final Presentation: Dustin,Anindo,Harlan,Giovanni |

Monday 12/11 | Course Conclusion |

plt17/top.txt · Last modified: 2017/12/03 20:04 by hossein