Syllabus

1 Course Description

This course is about formal specification, and how logic can be used to help reason about software. Logic is presented from a computational perspective using a variety of formal methods tools, from property based testing frameworks which exist in nearly every programming language, to SMT solvers that are becoming increasingly important across a variety of domains, to interactive theorem proving using the Lean theorem prover.

We focus on formal methods tools in order to show how logic can be used to actively reason about software, rather than existing as a purely theoretical pursuit off to the side. Clearly, logical reasoning has value even outside of the context of the types of tools that we will use, but we think that these tools will allow us to gain a much more hands-on understanding of it than via a more traditional presentation.

The goal of the course is to introduce fundamental, foundational methods for both modelling and reasoning formally about computation. We want to be able to talk precisely about what programs should do, and once we learn how to express ourselves in precise specifications, we will deploy an array of tools to use those specifications to increase the reliability of the programs we write.

We will draw upon propositional, first order, and higher order logic, and use equational reasoning and induction over recursive programs. We will talk about the strengths and limitations of various techniques, and how they can be applied to different problems.

2 Course Objectives

The goal of the course is to introduce students to the logic and specification using the field of formal methods. While there are many human processes for increasing the reliability of software, formal methods begins from the premise that we can use math and computation to make software more reliable scientifically.

Students will learn how to formulate specifications in a variety of ways, from executable predicates in property based testing frameworks that they can bring to any programming language they use, to finitized problems that can be translated into SMT queries and solved by off-the-shelf solvers, to rich higher-order logic specifications that can only be expressed and reasoned about within theorem provers.

Every step of the way, we will be running code, querying the solver, or interacting directly with the theorem prover, and so students will get hands-on experience with these state-of-the-art tools. In addition to learning how to use them, they will learn when each is best applied, a skill they can take to further studies, coop, or beyond.

3 Prerequisites

The course requires CS2500 (Fundamentals of Computer Science 1) and CS1800 (Discrete Structures). If you do not have this background, you need to get permission of the instructor.

4 Course Websites / Tools

4.1 Website

This website will be the main place that all course materials will be: homework assignments, lecture notes, etc. Please check it regularly.

4.2 Canvas

We will use Canvas for storing grades. You will not submit anything through Canvas. However, Canvas is the way to get to the various other tools, below.

4.3 Piazza

We will use Piazza for questions and discussion. While we will do our best to answer questions asked there, TA office hours are usually a much more reliable way to get help. You can connect to Piazza by going to Canvas and clicking the link in the sidebar.

4.4 Gradescope

You will use Gradescope to submit homework assignments, and the feedback you will get will be available on Gradescope. Like Piazza, you can get to Gradescope from Canvas.

4.5 Polleverywhere

We will use Polleverywhere for in-class quizzes. You can get to it, and link your account to it, from Canvas.

5 Software Used

5.1 ISL-Spec (and Quickcheck)

The first portion of the course introduces property based testing and specification using a language ISL-Spec which extends the Intermediate Student Language with Lambda (ISL+) language used at the end of CS2500 with support for testing using the Quickcheck library. If it’s been a while since you took CS2500, please refamiliarize yourself with ISL+ as we won’t spend a lot of time reviewing basic functional programming in class.

5.2 Rosette

The next portion of the course covers SAT/SMT solvers, staying within DrRacket but using the language Rosette, a state-of-the-art solver-aided programming language. We will only cover its use for verification of software, but curious students can explore how it can be used to also synthesize programs satisfying specifications.

5.3 Lean

The bulk of the course will then be spent with the theorem prover Lean, from Microsoft Research. Lean is an industrial strength tool used to program and prove properties about programs using higher-order logic. We will use Lean 4, the latest version under development, unlike previous iterations of the course, which used Lean 3.

6 Evaluation

Your final grade will be (TENTATIVELY) calculated as follows:

We will drop at least the lowest two homework grades, and your lowest ~1/3 quizes/worksheets (we’re aiming for very small, nearly daily ones, which would amount to at least 30, with at least 10 dropped). Further, if your Exam 2 grade is higher than your Exam 1 grade, we will drop your Exam 1 grade and count your Exam 2 grade for 40%. Since the material is somewhat cumulative, this is intended to reward those that improve over the course of the semester; it is not a reason to skip Exam 1!

Final grades will be assigned on the following scale:

6.1 Homework

Homework is a way to practice the material that you learn in lecture, and the main way you will learn the material. In is primarily a learning tool, and secondarily an assessment (i.e., grading) tool. You can work on homework in groups (of any size), or alone, and you can get help from anyone else in the class (or not in the class). This is a relatively unusual collaboration policy! The only requirement is that you write down the names of anyone that you talked with about your solution ( doesn’t need to include those in your group, as you’d be submitting one assignment as a group). Generally there will be one homework assignment due each week.

6.2 Quizes/Worksheets

We will have regular, small, in-class quizes or worksheets. These will happen most classes, and are intended to check your understanding and ensure you are keeping up with the material. They will also be used by the instruction team to flag topics that need to be covered in more depth. These will be quick, and should be straightforward if you are doing the homework and following the material for lecture. To allow flexibility, we will drop the lowest ten of them (which will be about 1/3).

6.3 Exams

There will be two exams. Dates TBD. They will be proctored and in-person, though will be done on individual computers (not on paper).

7 Policies

7.1 Late Work

We do not have any default allowance for late work: instead, we build in an allowance for things happening by dropping your two lowest scores, so that if something happens, it won’t adversely affect your grade. However, if an unusual situation happens, please reach out to the instruction team and we may be able to make an exception.

7.2 Regrades

Sometimes mistakes can happen and so if you are confused or concerned about feedback, please don’t be afraid to reach out to a member of the instruction team for further explanation. You must submit any requests for regrading at most 7 days after the feedback was released.

When you have a regrade request you should first reach out to the individual who graded your work. If the individual is unable to address your concerns you can approach your lecture instructor for further assistance.

7.3 Collaboration

Unlike in many classes, in this class, you are welcome to work on homework with anyone that you would like. If you want to talk to a friend, that is fine. If you want to talk to someone who took the class previously: also fine. As described in the section on homework, you are also free to work in groups, or alone, and to change groups from homework to homework There is only one thing you must do: include the names / emails of everyone that you work with in the file that you turn in (if you are turning in a group assignment, you don’t need to include the group members, as that’s obvious). Please err on the side of caution: even if you only work on part of the homework with them, or substantially change what you’ve done after, include their name. This collaboration will have no affect on grading; the names are simply a way of responsibly recording where you found help.

We do this because working with others can often be one of the best ways to learn, and we’d love if you can benefit from peers as much as you can from the instruction team. Homework is one of the primary tools for learning this material, and we don’t want to take any learning opportunities away from you.

That also cuts in a different direction. If you use the collaboration policy to primarily turn in solutions that you do not fully understand yourself, you will likely suffer in the in class quizes/worksheets and on the exams, which together account for 80% of your grade. So throw away the learning opportunity of homework at your own peril, as trying to "game" this collaboration policy is not a good way to be successful in the class.

8 Classroom Environment

To create and preserve a classroom atmosphere that optimizes teaching and learning, all participants share a responsibility in creating a civil and non-disruptive forum for the discussion of ideas. Students are expected to conduct themselves at all times in a manner that does not disrupt teaching or learning. Your comments to others should be constructive and free from harassing statements. You are encouraged to disagree with other students and the instructor, but such disagreements need to respectful and be based upon facts and documentation (rather than prejudices and personalities). The instructor reserves the right to interrupt conversations that deviate from these expectations. Repeated unprofessional or disrespectful conduct may result in a lower grade or more severe consequences. Part of the learning process in this course is respectful engagement of ideas with others.

8.1 Title IX

Title IX of the Education Amendments of 1972 protects individuals from sex or gender-based discrimination, including discrimination based on gender-identity, in educational programs and activities that receive federal financial assistance.

Northeastern’s Title IX Policy prohibits Prohibited Offenses, which are defined as sexual harassment, sexual assault, relationship or domestic violence, and stalking. The Title IX Policy applies to the entire community, including male, female, transgender students, faculty and staff.

If you or someone you know has been a survivor of a Prohibited Offense, confidential support and guidance can be found through University Health and Counseling Services staff (https://www.northeastern.edu/uhcs/) and the Center for Spiritual Dialogue and Service clergy members (https://www.northeastern.edu/spirituallife/). By law, those employees are not required to report allegations of sex or gender-based discrimination to the University.

Alleged violations can be reported non-confidentially to the Title IX Coordinator within The Office for Gender Equity and Compliance at: mailto:titleix@northeastern.edu and/or through NUPD (Emergency 617.373.3333; Non-Emergency 617.373.2121). Reporting Prohibited Offenses to NUPD does NOT commit the victim/affected party to future legal action.

Faculty members are considered "responsible employees" at Northeastern University, meaning they are required to report all allegations of sex or gender-based discrimination to the Title IX Coordinator.

In case of an emergency, please call 911.

Please visit https://www.northeastern.edu/titleix for a complete list of reporting options and resources both on- and off-campus.

8.2 Students With Disabilities

Students who have disabilities who wish to receive academic services and/or accommodations should visit the Disability Resource Center at 20 Dodge Hall or call (617) 373-2675. If you have already done so, please provide your letter from the DRC to me early in the semester so that I can arrange those accommodations.