Location

Tue, Fri 9:50AM-11:30AM Cahners Hall 002

Contact Information

Professor: Pete Manolios
Office hours: Tue 3:30PM-5:00PM in WVH 346 and by request
Email:

TA: Ankit Kumar
Office hours: TBD in TBD and by request
Email:

Goals

By the end of this course, you will:

1. Understand a selection of fundamental concepts and algorithms in the area of computer-aided reasoning.
2. Implement and evaluate a computer-aided reasoning system from scratch.
3. Be able to formalize computational systems at various level of abstraction.
4. Be able to effectively use a major theorem prover to mechanically prove non-trivial theorems about computational systems.

Course Structure

The course will consist mostly of lectures. There will be opportunities for students to give presentations. The class is project-based; you learn by doing and there will be pleny of learning.

Textbooks

We will use the following textbooks

1. Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press. The code accompanying the book can be found here.
2. Manolios. Reasoning about Programs (I may update this during the semester).

Software

Install and familiarize yourself with the following.

1. The ACL2 Sedan
2. A Common Lisp compiler such as SBCL or Clozure Common Lisp
3. Emacs

Reference Material

The following links provide useful references. I may add more links during the semester.

1. The ACL2 Documentation
2. Steele. Common Lisp the Language, 2nd Edition. This is available online from various sources, including this one
3. Emacs
4. Data Definitions

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 and projects 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 the projects or 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 Knuth-Bendix completion on this set of rewrite rules?"

Homework Assignments

This course will have regular project-based homework assignments requiring you to implement techniques and algorithms covered in class. Over the course of the semester, you will implement and evaluate a modular reasoning engine for a formal modeling language that can be used to model computational systems. Homework assignments will be done by groups of 2-3 students and will involve design, teamwork, and the implementation and evaluation of complex algorithms. To collaborate effectively, you should all be involved in all aspects of the homework problems. Homeworks will be marked 20 points off per day that they are late, up to 2 days. Important: You are responsible for finding a partner. The class forum located on Piazza is a particularly good resource for this, as there will be a thread there that serves exactly this purpose. Right before or right after lecture are also good times to look for partners. Submission instructions and more information can be found by clicking on the Assignments tab on the left. Any requests for grade changes or regrading must be made within 7 days of when the work was returned. To ask for a regrade, specify (a) the problem or problems you want to be regraded, and (b) for each of these problems, why you think the problem was misgraded.

Exams

There will be two exams. The current schedule is as follows, but it may change, given the situation we find ourselves in. The first exam will be given on 10/21 and will be an in-class exam. The second exam will be given on 12/2 and will be an in-class exam.

Presentations

Every student will pick 1-2 relevant research papers that they find interesting and will read and present them to the class. The presentation should include a motivation, it should relate the presented material to the material covered in class and it should explain why the topic is important and interesting.

Projects

Students have to propose a project that I will review and approve. Projects allow you to gain hands-on experience on a topic of interest. I suggest first choosing a project topic and then selecting a paper on this topic for your presentation. Your project can be theoretical, say coming up with a new algorithm, or it can involve the implementation of an interesting algorithm, or it can involve the use and evaluation of existing tools.

Evaluations

Graduate students will be responsible for evaluating one class assignment. This requires coming up with an evaluation plan for both the theoretical and practical parts of assignments. When evaluating algorithms, a test suite that stresses the algorithms will be created and used to run a competition between the student submissions. Feedback will be provided to students and the process will happen in a timely fashion (ideally one week after submission deadlines). Evaluators get an automatic A for the assignment they are evaluating.

Grading

The breakdown of the grades in this course for undergraduate students is as follows.

1. 30% Exams
2. 30% Homeworks
3. 15% Paper presentation
4. 15% Project
5. 10% Class participation

For graduate students grades are determined as follows.

1. 30% Exams
2. 25% Homeworks
3. 15% Paper presentation
4. 15% Project
5. 10% Class participation
6. 5% Evaluations

Academic Integrity

It's OK to ask someone about the concepts, algorithms, or approaches needed to do the assignments. We encourage you to do so; both giving and taking advice will help you to learn. However, what you turn in must be your own, or for projects, your group's own work; copying other people's code, solution sets, or from any other sources is strictly prohibited, unless you are explicitly given permission to do so. In particular, looking at other solutions (e.g., someone else's solution to a similar project) is a direct violation of our academic integrity policy. The project assignments must be entirely the work of the students turning them in. If you have any questions about using a particular resource, ask me. All students are subject to the Northeastern Academic Integrity policy. All cases of suspected plagiarism or other academic dishonesty will be referred to the Office of Student Conduct and Conflict Resolution (OSCCR) and to the college. In addition to any penalties imposed by OSSCR and the college, any violation of the academic integrity policy will result in an F for the course.

Accommodations for Students with Disabilities

If you have a disability-related need for reasonable academic accommodations in this course and have not yet met with a Disability Specialist, please visit the Northeastern Disability Resource Center and follow the outlined procedure to request services. If the Disability Resource Center has formally approved you for an academic accommodation in this class, please present the instructor with your "Professor Notification Letter" during the first week of the semester, so that we can address your specific needs as early as possible.

Schedule

The schedule below will be updated as the semester progresses. The list of topics we will cover includes: history of logic, data definitions, property-based testing, the ACL2s language, logic and theorem prover, propositional logic (PL), analysis (transformations, representations, decision procedures) of PL, equational reasoning, induction, generalization, the ACL2 waterfall, congruence-based reasoning, term rewriting (basic concepts, termination, confluence, Knuth-Bendix), using ACL2s effectively (the method, state, macros, books), FOL (First order logic) and major results (syntax, semantics, Skolemization, compactness, Herbrand universes, completeness, incompleteness, decidability, theorem proving), SMT solving, and reasoning about computation. As the semester progresses, I will be adding reading material. Please read the material before class. I will also add lecture materials.

Week	Topics
9/5	TOPICS Introductions. A brief history of logic, formal methods and the birth of computer science. A brief history of ACL2 and ACL2s. SLIDES & CODE Lecture 1 Slides
9/12	TOPICS Describing and reasoning about computation with ACL2s: An overview of the universe, specifying types with defdata, defining functions with definec, defining properties and testing them using counterexample generation and property-based testing. Definitions in ACL2s. Invariants, Contracts, Static/dynamic checking, Termination, Measure Functions. READINGS (1) Data Definitions (2) RAP: Chpts 1-3,5 (3) Harrison: Chpts 1, 2.1-2.6 (Can ignore OCaml code) SLIDES & CODE Lecture 2 Slides, Lecture 2 Code Lecture 3 Slides, Lecture 3 Code
9/19	TOPICS Equational Reasoning. Induction, Lemmas, Generalization, Professional Method. READINGS (1) RAP: Chpts 4,6 SLIDES & CODE Lecture 4 Slides, Lecture 4 Code Lecture 5 Slides
9/26	TOPICS Organization of ACL2, waterfall, decision procedures, congruence-based reasoning, term rewriting in ACL2, how to use the theorem prover, the method. ACL2s: Proof builder, Macros, State, world, using books, developing libraries, performace issues READINGS (1) RAP: Chpt 7 (2) Introduction to the Theorem Prover and all of the subtopics. SLIDES & CODE Lecture 6 Slides, Lecture 6 Code Lecture 7 Code
10/3	TOPICS PL satisfiability solving, Tseitin transformation, 2SAT, applications, DP, DPLL, BDDs. Presentation and Project discussion. READINGS (1) Harrison: Chpts 2.7-2.11 SLIDES & CODE Lecture 8 Slides Lecture 9 Slides
10/10	TOPICS First order logic: role as foundation of math, syntax and semantics, models, consequence, sat, validity, formalization examples. READINGS (1) Harrison: Chpts 3.1-3.6 SLIDES & CODE Lecture 10 Slides Lecture 11 Slides
10/17	TOPICS Prenex normal form, Skolemization. Reducing FO validity to universal fragment. Exam 1. READINGS (1)Harrison: 3.7-3.8 SLIDES & CODE Lecture 12 Slides Exam 1
10/24	TOPICS Propositional Compactness. Herbrand Universes. Reducing FO validity to propositional logic. Herbrand Interpretations. Quantifiers in ACL2. READINGS (1) Harrison: Chpts 2.12, Chpts 3.7-3.8 (2) Quantifier Tutorial and all of the subtopics. (3) Quantifiers and all of the subtopics. SLIDES & CODE Lecture 13 Slides, Lecture 13 Code
10/31	TOPICS Project/presentation previews and discussion. Unification: Algorithm, Termination. Unification: Correctness, Optimizations. READINGS Harrison: Chpts 3.9 SLIDES & CODE Lecture 14 Slides Lecture 15 Slides
11/7	TOPICS FO checking with unification/resolution. Godel's completeness and incompleteness theorems. SMT. READINGS Harrison: Chpts 3.11, 6.8, 7.4 SLIDES & CODE Lecture 16 Slides
11/14	TOPICS Refinement. Paper Presentations (See Piazza for schedule) READINGS None SLIDES & CODE Lecture 17 Slides
11/21	TOPICS Presentations (See Piazza for the schedule). READINGS None SLIDES & CODE
11/28	TOPICS Temporal Logic, Model-Checking. Project Presentations (See Piazza for the schedule), Exam 2 READINGS SLIDES & CODE Lecture 18 Slides
12/5	TOPICS Project Presentations (See Piazza for the schedule) READINGS None SLIDES & CODE