CS156: The Calculus of Computation, Autumn 2008

Decision Procedures with Applications to Verification
Meets Monday, Wednesday at 11:00-12:15 PM in GatesB12

Staff

Lecturer

Prof. Zohar Manna
Office Hours: MW 12:30-1:00 Gates 481

TAs

Boyu Wang
Office Hours: M 3:00-5:00 Tu 3:30-5:00 at Durand 1st floor lounge

Greg Goldgof
Office Hours: F 3:00-5:00 at Durand 1st floor lounge

Jason Auerbach (for matters related to piVC and the piVC assignment)
Office Hours: 12:30-2:00 on Wed Nov 5 and Fri Nov 7. Myth cluster.

Textbook

The Calculus of Computation:
Decision Procedures with Applications to Verification
Aaron Bradley
Zohar Manna
Springer 2007

Grading

Homeworks (60%) (8 in total)

Final exam (40%)

Topics

Overview

  1. First-order logic
  2. Specification and verification
  3. Satisfiability decision procedures

Part I: Foundations

  1. Propositional Logic
  2. First-Order Logic
  3. First-Order Theories
  4. Induction
  5. Program Correctness: Mechanics

Part II: Algorithmic Reasoning

  1. Quantified Linear Arithmetic
  2. Quantifier-Free Linear Arithmetic
  3. Quantifier-Free Equality and Data Structures
  4. Combining Decision Procedures
  5. Arrays