Location

Tue, Fri 1:35PM-3:15PM Robinson Hall 107

For Instructors and TAs, click on Contact Info on your left.

Goals

By the end of this course, you will:

1. Understand how logic is used to specify the semantics of a simple functional programming language.
2. Learn how to formally specify contracts, invariants and properties of programs.
3. Know how to use property-based testing to gain confidence in the correctness of programs.
4. Explore Boolean logic and its applications, including to security.
5. Understand and effectively use various proof techniques to reason about programs, including propositional reasoning, case analysis, proof by contradiction, instantiation, equational reasoning and induction.
6. Learn how to write rigorous paper and pencil proofs, as well as mechanized proofs that require lemmas and generalization.
7. Understand the distinctions between P/NP and decidability/undecidability.
8. Understand basic undecidability proofs based on Cantor diagonalization.
9. Learn how to prove termination of code using measure functions and generalizations based on infinite numbers.
10. Explore some of the considerations involved in formally reasoning about imperative programming languages such as C and Java.
11. Learn how to reason about simple imperative programs using loop invariants.
12. Explore the connections between termination and induction.
13. Learn how to formally reason about algorithms and how to prove functional equivalence of programs.
14. Explore refinement and observational equivalence.
15. Learn how to use logic to evaluate informal arguments by identifying hidden assumptions, inconsistencies, fallacies and the logical structure of such arguments.

Books and Supplies

The course book will be freely distributed to you during the semester. Click on Lecture Notes on your left.

An optional book that includes a lot of exercises is: Computer Aided Reasoning. Kaufmann, Manolios, Moore. You can order it from here. Please note that the book was written for at least upper level undergraduate students, so expect parts of the book to be hard. Also, in class we use ACL2s, a version of ACL2 that includes contracts and lots of other things that are not mentioned in the book. Nevertheless, this is the standard reference for ACL2 and contains many exercises whose solutions are available online.

Software

We will be using the ACL2s system. Please download it and install it on your machines, using the instructions here. It is also available on the Khoury Virtual Desktops, which allow you to run ACL2s with only a browser.

Forum

I will provide a Piazza-Based Web forum that can be used by students to ask questions and exchange wisdom while completing the homeworks in this course. You are expected to check it every day (you can configure it to send you daily updates), participate actively, and use it as a first place to post questions related to homeworks in this course. Please use the forum to post questions and answers that may be useful to others. Specifically, clarification questions about the homework, such as "What is the precise interpretation of homework question 2b" should be posted on the forum. Also, any questions at all about the material covered in class should be posted on the forum, e.g., "What do I wind up with when I apply the induction scheme for foo on this conjecture?"

Exams

There will be two exams. They will take place at the following times:

• Tue, Nov 1
• Fri, Dec 2

There is no final.

Grading

Grades will be determined as follows.

• Homeworks: 20%
• Exam 1: 25%
• Exam 2: 30%
• Quizzes: 20%
• Class Participation: 5%

Quizzes will occur regularly. Be prepared for a short quiz every day. Quizzes will probably happen using Canvas. Only a subset of the quizzes might be graded. If you are not present for a quiz or if you do cannot log in to Canvas, you will get 0 points. We will drop the lowest 10% of quizzes.

Homeworks will be given about once a week. Your homework grade will be based on your top ten homeworks. You will mostly work in groups. We will give you instructions on group sizes and composition. We recommend that you to first try to solve the problems on your own. Then meet with your partners to go over your solutions and solve any unresolved problems. We may only grade a subset of the problems assigned. Homeworks will be due on Wednesday at 11:00PM, unless otherwise noted.

Grading Notes

• You can take 1 double-sided sheet of paper to each exam.
• You have exactly 1 week after any assignment, or exam is graded to challenge your grade. After that, we will not change your grade.
• You are responsible for making sure that we entered the right points on canvas. If you notice any data entry errors, please inform us right away.

Prerequisites

CS 1800 and CS 2500.
If you do not have this background you should get the permission of the instructor. Our policy is that we do not grant exemptions if you did not getting passing grades in both the prerequisites: experience has shown that this is the best policy for students.

Academic Integrity

Read and intimately familiarize yourselves with the Northeastern Academic Integrity policy.

Warning: We do not tolerate any violations. If we believe that you violated the policy, we will report you to the university and to the college. On top of that, your grade for the course will be reduced to an F. Note that the university and the college can impose further penalties, including not allowing you to go on co-op; even expulsion from the university is possible in severe cases.

For example, here is something you cannot do, but again, read the full policy, the course contract and see Mitch Wand's Web page on the topic.

Unauthorized Collaboration: The University defines unauthorized collaboration as instances when students submit individual academic works that are substantially similar to one another. While several students may have the same source material, the analysis, interpretation, and reporting of the data must be each individual's independent work.

You can only collaborate with your partners on homework problems. Besides staff, the use of any other sources for homework solutions is a violation of the academic integrity policy. For exams you have to work alone and cannot use any resources beyond those explicitly allowed.

If you have any doubts at all whether something is allowed or not, please ask! For example, you can (and are encouraged to) discuss the material we cover in class with anyone. Collaboration, interaction, debate and discussion is encouraged, except for graded work as outlined above.

Class Guidelines, Policies and Notices

• If you don't understand something, please ask questions. We love questions. One of the benefits of attending a university as opposed to reading a book is that you get to interact with faculty.
• Give us feedback. Tell us what works; what doesn't. Tell us what you like about the class and what you don't like.
• In class, stay engaged during the lectures. There are only three hours of lectures a week and we want your undivided attention. Therefore, the use of electronic devices (computers, phones, etc) for non-class purposes is strongly discouraged. Recordings of class are not allowed.
• We will be fair with everyone, so rest assured that all the students will play by the same rules. To that end, we have clear policies. Make sure you understand them, as they apply to everyone in the class. For example, late homeworks will not be accepted under any circumstances. If you ask us to make an exception for just you, the answer will be no. If you ask us to change the due date for everyone and there is a good reason to do so, then we will consider it.
• Please feel free to question the policies; if you suggest improvements, we can change our policies (and have done so in the past).
• Using logic is the most foundational way to reason about computation and that is what we will spend most of the semester examining. But, logical reasoning is also useful for analyzing mathematics, science, politics, social sciences, public policy, philosophy, psychology, humanities, history, culture, biology, medicine, law, religion, the arts and any arguments that involve evidence and inference. We will spend some of our time considering arguments and the applicability of logic in this broader context. To that end, we may discuss and evaluate topics that you find challenging or that may cause you some discomfort. That is a feature, not a bug: a good education should involve rigorous exploration and debate. We will endeavor to do this in a civil, respectful way, as our ultimate goal is to understand the structure of various arguments, irrespective of whether we agree or endorse such arguments.