Here is a description of the verification project

Here are notes on verification, a supplement to the material in Chapter 3 of Hu!th and Ryan.

Here are roadmap for the unit on LTL, including notes on preparing for Quiz 4.

Here is a paper on automata-based verification referred to in the notes. This is optional reading, for those who want to go further and understand Buchi automata and verification at a level deeper than we have presented in class.

Here are the lecture notes on predicate logic, to serve as a supplement to the treatment in the text. (It doesn't replace the text, just use these notes as additional explanation in case it is useful.)

Here are the notes on predicate tableaux. This serves as a replacement for section 2.3 in the text.

Here is a review of basic computability.

Here are notes on the undecidability of predicate logic.

Here are notes on preparing for Quiz 3.

Here is the paper by Hantao Wang on using SAT-solving to build basetball schedules.

Here are the notes on propositional tableaux. This serves as a replacement for section 1.2 in the text!

The course information page gives information about: course objectives and prerequisites, grading, the textbook, course staff and office hours, and academic honesty and collaboration guidelines.

The weekly schedule page has the day-to-day schedule, including exam dates and reading assignments.

See the Problems page for problems to do to prepare for individual quizzes.

This class can be counted towards the BS/MS program. Details can be found here