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

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

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 (60%) and a final project (40%).

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

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.