about

Instructor:

Ben Delaware

bendy at purdue.edu

Office Hours: Mondays 2:30-4:00p in LWSN 2116M

Teaching Assistant:

Robert Dickerson

dicker18 at purdue.edu

Office Hours: Wednesday 2:00p-3:00p in HAAS 143

Course Description:

This is a graduate course on the logical foundations and algorithmic techniques used to ensure that programs do what they are supposed to do. We will focus on two key aspect of automated reasoning:

1. Specification: logics to define the expected behavior of a program in a machine-readable form,
2. Verification: methods to automatically check if a program meets its specification.

The course will be an exploration of both the theory and practice of automated computer-aided reasoning, and its application to reasoning about program behavior. Our exploration will cover a breadth of reasoning techniques and tools currently in use, e.g. SAT/SMT solvers, examining them from the both an implementation and user perspective.

logistics

Lectures:

Lectures will be Mondays, Wednesdays, and Fridays in LWSN 1106, which students are expected to attend. If you are sick or otherwise unable to attend a lecture, please let the instructor know as soon as possible. All lecture materials, including slides and related readings, will be made available on brightpsace after class.

Office Hours:

Each Monday, the instructor will have office hours from 2:30-4:-0p in LWSN 2116M, and the TA will hold office hours in HAAS 143 every Wednesday from 2:00-3:00. In the event that students cannot attend scheduled office hours, they should contact the instructor via email to schedule a time to meet individually.

Homeworks:

Homeworks will be posted (roughly) every three weeks, according to the course schedule. Homeworks are to be submitted via Brightspace by 6PM on their assigned due date. Make sure that any programs compile without errors (and ideally without any warnings). If they do not, they will not be graded. Everyone will receive three courtesy late days for the semester. Once all these days have been used, students will need to notify the instructor or the TA ahead of time with an explanation and plan for completion. These requests will be accepted at my discretion and may include a point penalty of 5% per day late. Asking for an extension does not guarantee it will be granted.

Course Project:

The course project has teams of 2-3 students toimplement a project of their choosing. As these projects are less structured than the homeworks, there will be three milestones to help keep everyone on track. A list of project ideas and a timeline will be posted on Brightspace.

success

How to Succeed in this Course

In order to be successful, students should be familiar with:

1. Programming in an imperative language, e.g. Java / C / Python, etc.
2. Basic logic and proofs techniques found in an undergraduate discrete math course like CS182: sets, relations, functions, proof by induction, proof by case analysis; recursion; and propositional logic.
3. The sorts of basic data structures and algorithms encountered in an undergraduate course like CS 251, e.g. lists, trees, heaps, graphs, sorting, graph traversals, and search.

We'll briefly review important concepts as needed, but this will be a refresher and not an introduction.

resources

Course Texts:

The main textbook for the course will be:

1. Bradley, Aaron R., and Zohar. Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. 1st ed. 2007. Online access from Purdue libraries

This will be supplemented with a variety of sources, including:

1. Nielson, Flemming, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis. 1st ed. 1999. Online access from Purdue libraries
2. Biere, Armin. Handbook of Satisfiability. 2009. Online access from Purdue libraries
3. Clarke, Edmund M. et al. Handbook of Model Checking. Ed. Edmund M. Clarke et al. 1st ed. 2018. Online access from Purdue libraries
4. Cousot, Patrick. Principles of Abstract Interpretation. 2nd ed. 2021. Online access from Purdue libraries

In addition, a (dynamically updated) list of supplementary readings will be available on Brightspace.

Discussion Forum:

The course Ed Discussion site will serve as the discussion board; all course announcements will also be posted there. In lieu of emailing the instructor or the TA with any general questions about using Haskell / Rust or assignments, please post them to the discussion board so that any other students with the same question can see the answer.

policies

Grading:

Final grades will be assigned according to the following breakdown:

(tentative) schedule