CIS 301. Logical Foundations of Programming, Spring 2001.
General course information:
Teaching Assistant:Your teaching assistant is
(Email: firstname.lastname@example.org). Her office is in Nichols Hall 19J, where she
will conduct office hours on Mondays and Tuesdays at 9:30 - 10:30 A.M.
- Chapter 1:
- Declarative sentences.
- Pseudo code for a deterministic algorithm that computes an
equivalent conjunctive normal form for each formula of propositional
- Chapter 2:
- 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:
Copyright 2001 Michael Huth