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:

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.

Grade Policies

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

Course Schedule

Tentative list of course topics:

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 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.