Course Description

Class Times and Location

M,W,Th 4:35pm - 5:40pm, West Village H 110

Logistics & Rules of Conduct

Class sessions will be highly interactive. If you don't understand something, ask questions. If you go over the material at home and still something doesn't make sense, use one of the many options to follow up: Piazza, office hours, email. Try these options in this order until you succeed. Don't give up.

Points for homeworks, quizzes and exams will be entered on Blackboard. You are strongly encouraged to check that we enter the right points for you. If you notice any data entry errors, please inform us right away. You have exactly 1 week after the cause for your disagreement has emerged (usually the day points for assignments, quizzes, or exams are released). After that, we will not change points.

Communication

We will be using Piazza, a Q&A platform, for most communication in this class. This includes announcements from our side (therefore, you must check Piazza daily) and class discussion that is deemed to be of general interest. Such discussion may concern class material, homework clarifications, but also any general comments on what you like about the class, and what you don't like. Please avoid email in all these cases.

For any personal issues that require privacy, you can send an email to the instructor or the TA. Likewise, you may choose to post a private note on Piazza, in which case it will be visible to all instructors. We promise that in such cases, any reply will be private, too.

Software

We will be using ACL2s (for "ACL2 Sedan"), a version of the ACL2 Theorem Prover. Please download ACL2s and install it on your machines. The ACL2s website contains detailed installation instructions. We will practice using ACL2s in the second Lab.

Books and Supplies

All that we require you to purchase is a TurningPoint Responder Card RF (also referred to as the TurningPoint clicker). You will soon be able to purchase the card from the Northeastern University bookstore (it has been ordered). Once you have it, go to Blackboard and register the card. You can do that by logging in to the class, then clicking on Tools on the left, and then find and click on the TurningPoint Registration Tool. You have to bring the card to every class.

There is no required book. If you want a reference to ACL2 (not ACL2s!) that includes a lot of exercises (whose solutions are mostly available online), consider: Computer Aided Reasoning, Kaufmann/Manolios/Moore. You can order it from here. Note, however:

• The ACL2s version of ACL2 that we use in class includes contracts and other things that are not mentioned in the book.
• The book was written for at least upper level undergraduate students, so expect parts of the contents to be hard.

Quizzes and Exams

There will be quizzes, two in-class midterm exams, and one final. Details here.

Grading

The grading scheme for the class is composed of mandatory points
(homework, labs, quizzes, midterm exams, final) and experience points. The idea is that mandatory points are given for class components that you are expected to participate in, while experience points are "extra credit". To get the best possible grade in this class, it is sufficient to obtain all of the mandatory points. That, however, is neither easy nor necessary: using experience points for certain extra work you can try to compensate for a loss of mandatory points.

A. Mandatory points: Here is the percentage of each component's contribution to the mandatory part of your grade. Note that, as per the above rule, these percentages add up to 100.

• Homework: 20%
  
• Labs: 10%
  
• Quizzes and class participation: 15%
  
• Midterm exams: 25%
  
• Final exam: 30%
  

Quizzes: we  will only grade a subset of them. If you are not present for a quiz, you do not have your clicker, you show up just before the quiz, or you leave right after the quiz, you will get zero points.

Midterms: to cushion the impact of a "bad day", we will put double  weight on the better of your two midterm exams.
Example: suppose you get 90/100 on your first midterm but only 40/100 on your second. Your total midterm exam contribution will then be ⅔  × 90 + ⅓ × 40 = 73% , instead of (90+40)/2 = 65%.

B. Experience points: These are extra points awarded for substantial additional efforts like solving challenge problems that will be offered in class (and possibly for minor efforts like finding critical errors in the lecture notes). Again, these are extra points that you don't need to pursue, but you can use them to compensate for a lack of points in mandatory components. Solving challenge problems will also expand your horizon beyond the class material. These problems will be hard: don't rely on them as a cheap way of filling point gaps elsewhere.

We will measure the percentage of experience points you obtained, compared to the total number of experience points announced this semester. This percentage number will then be divided by 10; the result will be added to the total percentage score you have obtained for the mandatory components of the class. This means the maximum you can achieve by earning experience points is an extra 10 percentage points in your final score.
Example: suppose after all mandatory points you stand at 85%. You have obtained half the experience points. This will earn you 5 percentage points and result in a class total of 90%.

The cutoff points for letter grades are as follows:

A	A-	B+	B	B-	C+	C	C-	D+	D	D-	F
93	90	87	83	80	77	73	70	67	63	60	<60

In the example above, your experience points will thus elevate you from a B to an A- .

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

Warning: We do not tolerate any violations. If we suspect that you violated the policy, we will report you and the consequences can be as severe as expulsion from the university.

An example of an Academic Integrity violation that we have had problems with in the past and will therefore monitor carefully is:

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.