Logic and Computation
CS 2800 Spring 2020

Khoury College of Computer Sciences
Northeastern University
CS 2800 is a 4-credit course. The Office of the Registrar has useful information.


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

You are required to check for announcements daily.


Books and Supplies

There is no required book. If you want a reference that also includes a lot of exercises, then consider: 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 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.


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

Academic Integrity

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

Please read and sign the Course Contract.

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. If you remain in the class, your grade will be reduced, perhaps to an F, at our discretion. In addition 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 quizzes, the electronic device you use can only have the polleverywhere app/webpage open during quizzes. The use of lecture notes, ACL2s, or any other applications during quizzes is a violation of the academic integrity policy. Sharing information with other students, taking quizzes for other students or communicating with other students is also a violation of our academic integrity policy.


There are exactly two exams. They will take place at the following times: Let us know by January 15 if you have a conflict.


Grades will be determined as follows.

There are only 2 exams and there is no final.

Quizzes will occur regularly. Be prepared for a short quiz every day. Only a subset of the quizzes might be graded. If you are not present for a quiz or if you do not have Poll Everywhere working, 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 Monday at 10:00PM, unless otherwise noted.

You will spend most of your time in labs working on problems that we distribute in advance. If you solve the problems on your own before lab and are confident in your solutions, there is no need to show up. If you did not have time to solve the problems, or you tried and ran into trouble, then go to lab.

PollEverywhere Instructions

Sign up on the website using your Husky email account here.

In class, we will periodically ask you to respond to a poll. We will either provide a link to the poll or give you our PollEverywhere user name. To join any active poll, either click the provided link--or, if we give you our user name, you can click "Join a Presentation" when logged into PollEverywhere on your laptop or phone (if you install the PollEverywhere app).

If you use the app, log into PollEverywhere using your Husky email.

Grading Notes


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.


Jan 6
  1. Introductions & motivation, slides
  2. Syllabus, class webpage, programming review, slides
  3. Designing data-driven programs, the ACL2s development environment, slides, code
  1. None
  2. None
  3. None
Jan 13
  1. Basic data types, expressions, syntax & semantics of atomic data and associated primitive functions, slides
  2. Syntax & semantics of lists, design considerations of the ACL2s core language, contracts, termination, slides, code
  3. helpful function, quote, let, Datatypes: enumerated, range, product, record, union, list, (mutually) recursive, design recipe slides, code
  1. 2.1-2.4
  2. 2.5-2.10
  3. 2.11-2.13
Jan 20
  1. Property-based testing, test?, thm, program mode and defunc settings, slides, code
  2. Property-based testing in industry, Fuzzing, security applications, slides, code
  1. 2.14-2.17
  2. None
Jan 27
  1. Boolean logic, truth tables, characterization of formulas, Security: one-time pads, slides
  2. Introduction to P=NP, Properties of Boolean operators, Proof methods: instantiation, case analysis, equational proofs, decision procedures, slides
  3. Boolean logic in ACL2s, Normal forms, Set Theory connections, applications, slides
  1. 3-3.2
  2. 3.3-3.5
  3. 3.6-3.10
Feb 3
  1. Limitations of Boolean logic, intro to equational reasoning for programs, slides
  2. Axioms for equality, cons-first-rest axioms, definitional axioms, instantiation, contract checking and completion, slides
  3. On the computational nature of conjectures, using ACL2s to understand conjectures and counterexamples, equational reasoning with nested Boolean operators, slides
  1. 4
  2. 4.1
  3. 4.2-4.4
Feb 10
  1. Undecidability results, Reasoning about arithmetic, program equivalence: proving correctness of an exponential-time improvement, slides, code
  2. Context vs. theorems, derived context, numeric reasoning in C & other languages, slides, C code
  3. How to prove theorems using equational reasoning, formalization examples, proof examples, slides, formalization files, C formalization code
  1. 4.5
  2. 4.6
  3. None
Feb 17
  1. Definitions: soundness, termination, contracts, the ACL2s Definitional Principle
  2. Termination, measure functions, Review
  1. 5.1
  2. None
Feb 24
  1. Using termination to show soundness of common recursions schemes, big-Oh analysis as a refinement of termination
  2. Undecidability of halting problem
  3. Proof by contradiction, mathematical induction, well-foundnesses, a proof that mathematical induction works, how to extract induction schemes from admissible recursive functions
  1. 5.2-5.3
  2. 5.4-5.5
  3. 6-6.2
Mar 9
  1. Using induction to prove program correctness
  2. Data-function-induction trinity, Importance of termination
  3. Induction like a professional, reasoning about algorithms: sorting, correctness
  1. 6.3
  2. 6.4-6.6
  3. 6.7
Mar 16
  1. Classes cancelled due to coronavirus move out
  2. Generalization, lemma generation, dealing with induction failure
  3. Intro to reasoning about accumulators
  1. None
  2. 6.8
  3. 6.9
Mar 23
  1. Tail recursion: efficiency considerations, how to prove correctness
  2. Accumulator reasoning examples
  3. Abstract and algebraic data types
  1. 6.9
  2. 6.9
  3. 8.1-8.2
Mar 30
  1. Observational equivalence
  2. Reasoning about imperative programs: defining the semantics of a simple while language in ACL2s
  3. Reasoning about imperative programs using loop invariants; checking such proofs in ACL2s
  1. 8.3-8.4
  2. 9-9.2
  3. 9.3
Apr 6
  1. Reasoning about imperative programs and security, exam2 review
  2. Compiler correctness
  3. Mathematical logic: syntax, semantics, proof theory, undecidability, incompleteness, slides
Apr 13
  1. A look back: Logic and the birth of computer science; A look forward: what's next
  1. None