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 techniques, from property based testing which exists in libraries in nearly every programming language, to SMT solvers that are becoming increasingly important across a variety of domains, to particular runtime contract tracing that is coming directly from active research.

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 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, e.g., paper and pencil logic presentations you might find in a formal logic class in Philosophy.

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 techniques to use those specifications to increase the reliability of the programs we write.

We will draw upon propositional, first order, higher order, and substructural logics. 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 tracing contracts that can capture rich temporal properties.

Every step of the way, we will be running our assertions and getting feedback as to whether they hold, 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 technique 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 Discord

We will use Discord for announcements, 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 use this link to join:

https://discord.gg/F3QAPF7EMY

NOTE: You must set your display name on the server to your full name before we give you access to the (private) course channel.

4.3 Gradescope

You will use Gradescope to submit homework assignments, and the feedback you will get will be available on Gradescope. If you go to Gradescope and log in with Northeastern credentials, you should be enrolled in the class.

5 Software Used: Logical Student Language (LSL)

The course uses a language that we have developed specifically for it, Logical Student Language. It should be familiar from CS2500, as it is an extension of ISL+. The extensions allow us to expose you to state-of-the-art tools in a consistent setting, without any of the (typical) headache of getting various tools installed. It also avoids us having to teach you multiple different language syntaxes/semantics in order to expose you to different types of tools. What that does mean, however, is if it has 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.

6 Evaluation

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

Exams will be in-person, during class. Doing better on subsequent exams can raise your final score on earlier exams: essentially, we will take the maximum of the average of the exam and all that follow and the original score. Concretely, the formula (with examples) is:

(: exam1-final (-> Real Real Real Real))

;; the max of: original exam1 score, average of exam1 & exam2, average of all 3

(check-expect (exam1-final 95 90 90) 95)

(check-expect (exam1-final 80 100 85) 90)

(check-expect (exam1-final 80 90 100) 90)

(define (exam1-final exam1-raw exam2-raw exam3-raw)

(max exam1-raw

(/ (+ exam1-raw exam2-raw) 2)

(/ (+ exam1-raw exam2-raw exam3-raw) 3)))

(: exam2-final (-> Real Real Real Real))

;; the max of: original exam2 score, average of exam2 & exam3

(check-expect (exam2-final 100 80 75) 80)

(check-expect (exam2-final 90 80 90) 85)

(check-expect (exam2-final 70 80 90) 85)

(define (exam2-final exam1-raw exam2-raw exam3-raw)

(max exam2-raw

(/ (+ exam2-raw exam3-raw) 2)))

(: exam3-final (-> Real Real Real Real))

;; the original exam3 score

(check-expect (exam3-final 70 80 90) 90)

(check-expect (exam3-final 100 90 95) 95)

(check-expect (exam3-final 100 80 87) 87)

(define (exam3-final exam1-raw exam2-raw exam3-raw)

exam3-raw)

Final grades will then 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.

Half the homeworks will be done solo, and half of them can either be done solo or in groups of two. You must get the group approved by a TA or the instructor, and can only work with the same person for four assignments before you must switch (to another person, or to working solo).

Generally there will be two homework assignment due each week, due Tuesday & Thursday (at 9PM). The Thursday one will be solo, the Tuesday one (optionally) pair.

6.2 Exams

There will be three exams, held on 2/1, 2/29, and 4/10 (see Schedule for that and much more). They will be proctored and in-person.

7 Policies

7.1 Late Work

Any assignment can be turned in up to 24hrs late; you must notify the instructor (on Discord), but, provided this is not abused, this will always be granted. After that 24hrs, no work will be accepted (except in truly exceptional situations), so be sure to start early and try to get all the work done by the deadline. If you decide to treat the late deadline as the normal deadline (either using it every time, or asking for leeway on turning it in beyond the late deadline), expect not to be accomodated.

7.2 Regrades

Sometimes mistakes can happen. Please don’t be afraid to reach out to a member of the instruction team for further explanation. If you believe an error was made, you may make a regrade request: be precise about what exactly you believe was the mistake. Do not abuse this. You must submit any requests for regrading at most 7 days after the feedback was released.

You submit regrade requests directly via Gradescope – that will automatically go to the person who graded your work. If the individual is unable to address your concerns you can approach your instructor for further assistance.

7.3 Collaboration

You may discuss homeworks, including solutions, but may not either share or look at any code. You should keep your discussions to the approaches you took, ideas that are relevant, etc.

Homework is the primary way you learn the material, and if you share solutions, not only are you violating academic integrity, you are preventing the person you are sharing them with from learning the material. Note: you may not work around this policy by dictating solutions: this is effectively the same as sharing code.

This is a relatively flexible policy, which we follow 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 learning opportunities away from you.

That also cuts in a different direction. If you never figure out any solutions yourself and your conversations with others are always one-sided, you will likely suffer in the exams, which account for 66% of your grade. So be sure you are using this policy to improve your learning via homework, rather than using it to avoid the learning opportunity of homework, as trying to "game" this collaboration policy is not a good way to be successful in the class.

7.4 LLMs

You may not use LLMs (ChatGPT, or similar) for any portion of the course: assistance on homework, clarification of material, etc. They are, quite frankly, likely to lead you astray, rather than help you, and you are much better off making use of the resources provided by the course & course staff. Further: these tools will not be available during exams, which collectively compose 66% of your grade, so if you do manage to find a way for them to carry out some of the homework (again, extremely unlikely), you are only hurting yourself by not learning the material. As mentioned above, homework is the primary way that you will learn the course material, so any violations of academic integrity (whether via LLMs or other people) will only hurt you, as you cannot do well (or, possibly even pass) without learning the material sufficiently to demonstrate it, on your own, during the exams.

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.

This policy applies to all course-related spaces, including office hours, any exam reviews, and certainly the course Discord.

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.