COMP 403/503 - Reasoning about Software (Spring 2021)

Instructor: Konstantinos Mamouras
Class meetings: Mondays, Wednesdays and Fridays 9:45 am - 10:40 am (online)
Office hours: Tuesdays 11:00 am - 12:00 pm (online)

Teaching assistant: Zhifu Wang
Office hours: Thursdays 11:00 am - 12:00 pm (online)

Course Description

COMP 403/503 is an introduction to the field of formal methods, which develops methodologies for (1) precisely specifying the desired behavior of software, (2) formally reasoning about the execution of programs in order to provide guarantees of correctness, and (3) systematically exploring the corner cases of software execution in order to identify subtle bugs. In this class, we will study the theoretical foundations of systems for program analysis and verification, implement prototype versions of these systems, and perform case studies using existing tools.

Required Texts and Materials

We will not follow any one textbook in this course. The following references may be useful for parts of the course:

Grade Policies

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

Course Schedule

Tentative list of course topics:
Date Topic Readings
January 25 Introduction, Functional Programming Preface, Basics
January 27 Functional Programming Basics
January 29 Functional Programming Basics, Induction
February 1 Functional Programming Induction
February 3 Functional Programming Lists
February 5 Functional Programming Polymorphism
February 8 Logic Logic in Coq
February 10 Constructive Interpretation of Logic Logic in Coq
February 12 Inductively Defined Propositions IndProp
February 15 CLASS CANCELED due to storm
February 17 NO CLASS
February 19 CLASS CANCELED due to storm
February 22 Reasoning about Relations Relations
February 24 More about Relations Relations
February 26 Imperative Programming Winskel, Chapter 2
March 1 NO CLASS
March 3 Operational Semantics Winskel, Chapter 2
March 5 The Logic of Partial Correctness Winskel, Chapter 6
March 8 The Logic of Partial Correctness Winskel, Chapter 6
March 10 The Logic of Partial Correctness Dafny
March 12 The Logic of Partial Correctness Dafny
March 15 Propositional Logic BM, Chapter 1
March 17 Propositional Satisfiability BM, Chapter 1
March 19 Propositional Satisfiability BM, Chapter 1
March 22 First-Order Logic, Syntax BM, Chapter 2
March 24 First-Order Logic, Semantics BM, Chapter 2
March 26 NO CLASS
March 29 First-Order Logic, Sequent Calculus BM, Chapter 2
March 31 First-Order Theories, Quantified Linear Arithmetic BM, Chapters 3 and 7
April 2 Quantified Linear Arithmetic, Quantifier Elimination BM, Chapter 7
April 5 Quantified Linear Arithmetic, Quantifier Elimination BM, Chapter 7
April 7 Theory of Equality BM, Chapter 9
April 9 Theory of Equality BM, Chapter 9
April 12 Reasoning about Arrays BM, Chapter 9
April 14 Nelson-Oppen Combination Method BM, Chapter 10
April 16 Nelson-Oppen Combination Method BM, Chapter 10
April 19 Nelson-Oppen Combination Method BM, Chapter 10
April 21 The Z3 Theorem Prover Z3 Tutorial
April 23 Static Analysis NNH, Chapter 2
April 26 Static Analysis NNH, Chapter 2
April 28 Abstract Interpretation NNH, Chapter 4
April 30 Course Conclusion Notes on Canvas

Absence Policies

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

Rice Honor Code

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.

Disability Support Services

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.