CS156: The Calculus of Computation, Winter 2010

Final is on Monday March 15, 8:30 - 11:30 AM, in Gates B12

Server code for HW 8 is updated - you should now be able to run it from leland machines

HW 8 is due Friday midnight

Temporal logic final materials:

CD156 and CS256 topics: 6 slides (this is the introduction slides)
Lecture 1: 1-6 to 1-8 (always inclusive)
Lecture 2: 2-39 to 2-40
Lecture 3: 3-1 to 3-25, 3-27 to 3-29, 3-32 to 3-33
Lecture 4: 4-17 to 4-18
Lecture 5: 5-14 to 5-21 and 5-23 to 5-30

Selected slides from CS 256 is online

Server for HW 8 here

CS 256 - Introduction slide, Lecture 3 and 5 are online

Homework 8 is online

Lecture 8 is online

HW 7 is online

Final time is in the morning, staff email is cs156-win0910-staff@lists.stanford.edu

Lecture 7 and 9 are updated

HW 6 is online

Lecture 9 slides are updated (all of them are, but the others are trivial admin changes)

Final exam time posted. Location TBA

HW 5, lecture 7, 9, 10 are online

HW 4 is online

HW 3 is online. NOTE: The handout given in class has a typo. 3.4c should say 3.4b.

HW 2, Lecture 4 and 5 are online

Gary's office hour is updated

Clarification to HW 1, Q1.5d: Convert this formula into NNF, DNF, and CNF. Also, convert it into an equisatisfiable formula in CNF using the efficient method, and decide whether it is satisfiable.

Gary's temporary office hour is in Gates' 4th floor lounge, Monday 2:30 - 3:30

Grade distribution for homework and final is changed to 40% and 60%

Lecture 1 - 3, HW 1 are online

Welcome to CS 156

Index

Handouts

Date	Title
Jan 6	Fact Sheet	pdf
Jan 6	Lecture 1	full	2x2
Jan 6	Lecture 2	full	2x2
Jan 6	Lecture 3	full	2x2
Jan 6	Homework 1	pdf
Jan 11	Lecture 4	full	2x2
Jan 11	Lecture 5	full	2x2
Jan 11	Homework 2	pdf	soln
Jan 23	Homework 3	pdf
Jan 27	Homework 4	pdf
Feb 3	Homework 5	pdf
Feb 3	Lecture 7	full	2x2
Feb 3	Lecture 9	full	2x2
Feb 3	Lecture 10	full	2x2
Feb 14	Homework 6	pdf
Feb 17	Homework 7	pdf
Feb 24	Lecture 8	full	2x2
Feb 24	Homework 8	pdf	server
Feb 24	CS 256 - Introduction	full	2x2
Feb 24	CS 256 - Lecture 3	full	2x2
Feb 24	CS 256 - Lecture 5	full	2x2
Mar 3	CS 256 - Selected Lectures	full	2x2

Staff

Lecturer
Prof. Zohar Manna
manna@cs.stanford.edu
Office Hours: After Class

TAs
Gary Soedarsono
gary503@stanford.edu
Office Hours: Mon 3:00 - 4:00, Gates B26B, Tue 4:00 - 6:00, Gates B26A

Email: cs156-win0910-staff@lists.stanford.edu

Textbook

Grading Policy

Homeworks (40%) (8 in total)

weekly
due at the beginning of class (no late submissions without an extension)
no collaboration

Final exam (60%)

Monday, March 15, 08:30 - 11:30 AM, Gates B12 (Please email us if you have a conflict)

The temporal logic materials for the final are:

CD156 and CS256 topics: 6 slides (this is the introduction slides)
Lecture 1: 1-6 to 1-8 (always inclusive)
Lecture 2: 2-39 to 2-40
Lecture 3: 3-1 to 3-25, 3-27 to 3-29, 3-32 to 3-33
Lecture 4: 4-17 to 4-18
Lecture 5: 5-14 to 5-21 and 5-23 to 5-30

Syllabus

Decision procedures with applications to analyzing and developing robust software.
Logic review: Propositional and first-order logic; induction. (Chapters 1-4)
Verification: Methods for proving correctness of sequential programs using first-order reasoning; need for decision procedures. (Chapter 5)
Decision procedures: Algorithms that decide the validity of logical formulas for common theories including SAT, equality, arithmetic, recursive data structures, and arrays. (Chapters 7, 9, 11)
Combination theories and combination of decision procedures. (Chapter 10)
Projects include writing verified programs.
Overview of Temporal Logic and its application