**Instructor:**
Konstantinos Mamouras

**Class meetings:**
over Zoom ~~Mondays, Wednesdays and Fridays at 10:00 am - 10:50 am (Duncan Hall 1046)~~

**Office hours:**
over Zoom ~~Tuesdays 11:00 am - 12:00 pm at Duncan Hall 3081~~

**Teaching assistant:**
Agnishom Chattopadhyay (office: Abercrombie Laboratory C112)

**Office hours:**
over Zoom ~~Thursdays 2:00 pm - 3:00 pm at DH 3110~~

- Principles of Program Analysis. By Nielson, Nielson, and Hankin.
- The Calculus of Computation. By Bradley and Manna.
- The online volumes Logical Foundations and Programming Language Foundations of the Software Foundations series.
- The Formal Semantics of Programming Languages. By Winskel.

The grade will be based on homework assignments (60%) and a final project (40%).

- Functional programming languages and type systems
- Imperative programming languages
- Data flow analysis, type-based analysis and pointer analysis
- Abstract interpretation
- Random program testing
- Symbolic test generation
- Software model checking and refinement types
- Deductive verification
- Type theory and proof assistants
- Invariant synthesis
- Program synthesis

Date | Topic | Readings |
---|---|---|

January 13 | Introduction, Functional Programming | Preface, Basics |

January 15 | Functional Programming | Basics, Induction |

January 17 | Functional Programming | Induction, Lists |

January 20 | NO CLASS | |

January 22 | Functional Programming | Lists |

January 24 | Functional Programming | Polymorphism |

January 27 | Functional Programming | Polymorphism |

January 29 | Imperative Programming | NNH, Section 1.2 |

January 31 | Imperative Programming, Semantics | Winskel, Chapter 2 |

February 3 | Imperative Programming, Semantics | Winskel, Chapter 2 |

February 5 | Imperative Programming, Semantics | Winskel, Chapters 1-4 |

February 7 | Logic | Logic in Coq |

February 10 | The Logic of Partial Correctness | Winskel, Chapter 6 |

February 12 | The Logic of Partial Correctness | Dafny |

February 17 | The Logic of Partial Correctness | Dafny |

February 19 | Propositional Satisfiability | BM, Chapter 1 |

February 21 | Resolution for Propositional Satisfiability | BM, Chapter 1 |

February 24 | First-Order Logic, Syntax | BM, Chapter 2 |

February 26 | First-Order Logic, Semantics | BM, Chapter 2 |

February 28 | First-Order Logic, Sequent Calculus | BM, Chapter 2 |

March 2 | Quantified Linear Arithmetic | BM, Chapter 7 |

March 4 | Quantified Linear Arithmetic, Quantifier Elimination | BM, Chapter 7 |

March 6 | Quantified Linear Arithmetic, Quantifier Elimination | BM, Chapter 7 |

March 9, 11, 13 | CLASSES CANCELED | |

March 16, 18, 20 | SPRING BREAK | |

March 23 | First-Order Theory of Rationals | BM, Chapter 7 |

March 25 | Theory of Equality | BM, Chapter 9 |

March 27 | Theory of Equality | BM, Chapter 9 |

March 30 | Theory of Equality | BM, Chapter 9 |

April 1 | Reasoning about Arrays | BM, Chapter 9 |

April 3 | Reasoning about Arrays | BM, Chapter 9 |

April 6 | Tutorial: writing proofs | |

April 8 | Equational Logic, Combination of Theories | BM, Chapter 10 |

April 10 | Nelson-Oppen Combination Method | BM, Chapter 10 |

April 13 | Nelson-Oppen Combination Method | BM, Chapter 10 |

April 15 | The Z3 Theorem Prover | Z3 Tutorial |

April 17 | The Z3 Theorem Prover | Z3 Tutorial |

April 20 | Static Analysis | NNH, Chapter 2 |

April 22 | Static Analysis | NNH, Chapter 2 |

April 24 | Abstract Interpretation | NNH, Chapter 4 |

If a student misses a course meeting, they are expected to review the corresponding material on their own.

In this course, all students will be held to the standards of the Rice Honor Code, a code that you pledged to honor when you matriculated at this institution. If you are unfamiliar with the details of this code and how it is administered, you should consult the Honor System Handbook. This handbook outlines the University's expectations for the integrity of your academic work, the procedures for resolving alleged violations of those expectations, and the rights and responsibilities of students and faculty members throughout the process.

If you have a documented disability or other condition that may affect academic performance you should: 1) make sure this documentation is on file with Disability Support Services (Allen Center, Room 111 / adarice@rice.edu / x5841) to determine the accommodations you need; and 2) talk with the instructor to discuss your accommodation needs.