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

Instructor: Konstantinos Mamouras
Class meetings: over Zoom Mondays, Wednesdays and Fridays at 10:00am-10:50am (Duncan Hall 1046)
Office hours: over Zoom Tuesdays 11:00am-12:00pm at Duncan Hall 3081

Teaching assistant: Agnishom Chattopadhyay (office: Abercrombie Laboratory C112)
Office hours: over Zoom Thursdays 2pm-3pm 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:

Grade Policies

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

Course Schedule

Tentative list of course topics:
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.