about

Instructor:

Ben Delaware

bendy at purdue.edu

Office Hours: Mondays 12:30-2:00p in LWSN 3154L

Teaching Assistant:

Bekah Sowards

Office Hours: TBD

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 WALC 3154, 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 Brightspace after class.

Office Hours:

Each Monday, the instructor will have office hours from 12:30-2:00p in LWSN 3154L, and the TA will hold office hours at some point too! 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 two weeks, according to the course schedule. The written portion of each homework is to be submitted via Gradescope, and the programming portions should be submitted via Brightspace. All homeworks are due 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. There is no need to contact the instructor or the TA to use a late day-- they are automatically applied as soon as the due date has passed. 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