About

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.

Instructor

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

Office hours: By appointment.

Teaching Assistant

Abhinav Verma; averma8053@gmail.com; Duncan Hall 3137.

Office hours: By appointment.

Evaluation

The work for this course will have three components: (a) discussions and blog posts on research papers; (b) homework assignments; and (c) a final project.

Discussions and blog posts on research papers

A lot of the material that we will cover in this class is recent research and only appears in research papers. The class will alternate between a few lectures on background related to a topic, and student-led discussions on research papers. Each discussion will be led by a student and deeply discuss one paper. The responsibilities of the leader will be to:

• Summarize the content of the paper in a ~20 minute presentation (either on the whiteboard or using slides).
• Connect the content of the paper to real-world applications.
• Pose research questions related to the topic.
• After the class, write a 1000-2000 word blog post summarizing the paper and the discussion. 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 Abhinav, the post will be published on this website.

All other students will be expected to read the paper as well.  

Assignments

You will have to perform 4-5 assignments. These might include: (1) programming assignments,  (2) exercises using existing systems for reasoning about software, and (3) 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.

Project

There will also be a final project. This will be done in groups and follow up on the topics covered in student-led discussions. Specifically, each project will include:

• Reading and understanding a set of related research papers
• Using the ideas in the research paper for either building a program analysis/synthesis tool, 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.