**General course information:**

- Captain's log: see what was covered when.
- Course prerequisites and expected outcomes;
- Syllabus;
- a
**worldwide web tutor**, based on our textbook; - all assignments for this course;

**Ancillary material:**

**Chapter 1:**- Declarative sentences.
- Pseudo code for a deterministic algorithm that computes an
equivalent conjunctive normal form for each formula of propositional
logic:
- computing an implication-free formula;
- computing a negation normal form;
- computing a conjunctive normal form;
- the computationally expensive part: a subroutine that uses the distributivity law.

**Chapter 2:**- An example and explanation of the satisfaction relation for predicate logic.

**Chapter 3:**- An introduction to SMV: a puzzle;
- A discussion of fixed-point characterizations of those CTL connectives that reason about computation paths of two processes;
- A discussion of our SMV program for the mutual exclusion of two processes;
- Model Checking home page of the School of Computer Science at Carnegie Mellon University; and a manual for the programming language SMV by McMillan.

**Chapter 4:**- Sample programs of our core programming language;
- a program for the minimal-sum section of an integer array;
- a four-line program for which nobody (so far)
could prove
**termination**! - probabilistic program correctness and termination.

Copyright 2001 Michael Huth (huth@cis.ksu.edu)