Rice University logo

COMP 403/503: Reasoning about Software



Our reliance on software of all forms is increasing by the day. As a result, it’s more important than ever to ensure that programs are reliable, secure, and performant. The field of formal methods takes on this challenge, developing algorithms and programming methodologies that can be used: (1) to formally reason about what happens when programs execute on arbitrary inputs, and give guarantees of good program behavior, and (2) to systematically explore corner-case program behavior, and identify subtle bugs and vulnerabilities.

COMP 403/503 is an introduction to this field. In this class, we study the theoretical foundations of these systems; you will also implement prototype tools for reasoning about software, and perform case studies using existing tools.

Where and When

MWF 10:00am-10:50am; Duncan Hall 1046.


Swarat Chaudhuri; swarat@rice.edu; Duncal Hall 3103.

Office hours: By appointment.

Teaching Assistant

Lucas Martinelli Tabajara; lucasmt@rice.edu; Duncan Hall 3053.

Office hours: By appointment.


The work for this course will have three components: (a) blogging; (b) homework assignments; and (c) a final project.


We won’t use a fixed textbook in this class, because a lot of the material that we will cover is recent research and only appears in research papers. However, we will write a textbook, so to speak. More seriously, we will assign a scribe to each of the lectures. The role of the scribe will be to write a 1000-2000 word blog post on the topic covered in the lecture, in consultation with Swarat and Lucas. The post will distill the technical essence of the concepts covered in the lecture, give appropriate illustrations, and point to relevant references. Once approved by Swarat and Lucas, the post will be published on this website.


You will have to perform 4-5 assignments. These will include: (1) programming assignments, where you build program analyzers, (2) exercises using existing systems for reasoning about software, and (3) possibly, some theoretical exercises.

Programming assignments will be graded via an in-person codewalk, where every member of the coding team must be present. You must be prepared to answer questions related to design and implementation choices.

All assignments are to be completed and submitted individually.


There will also be a final project. This will be done in groups, and will have two components:

  • Reading and understanding a research paper
  • Using the ideas in the research paper for either an implementation for C program analysis/synthesis, or a detailed case study on a realistic benchmark.

The deliverables of the project will include a short (~3-4 page) writeup and a presentation.