Announcements

• 4/8/2004:
  Here is the reading assignment for Thursday, April 8th.
  1. Pnueli's Linear and Branching Structures in the Semantics and Logics of Reactive Systems
  2. Lattice theory and the Tarski-Knaster Theorem
  3. Manolios' Mu-Calculus Model Checking in ACL2

  The reading assignment for Tuesday, April 13th is:

  1. Brace et al's Efficient Implementation of a BDD package
  2. Manolios and Trefler's Safety and Liveness

  The reading assignment for Thursday, April 15th is:

  1. Paige and Tarjan's Three Partition Refinement Algorithms (only section 3 on the relational coarsest partition problem)
  2. Browne et al's Characterizing Finite Kripke Structures in Propositional Temporal Logic
  3. Manolios' A Compositional Theory of Refinement

• 3/25/2004: Here is the reading assignment for Tuesday, March 30th.
  1. Burch and Dill's Automatic Verification of Pipelined Microprocessor Control
  2. Manolios' Correctness of Pipelined Machines
  3. Manolios and Srinivasan's Automatic Verification of Safety and Liveness using WEBs

  The reading assignment for Thursday, April 1st is:

  1. Bryant et al's Modeling and Verifying Systems Using CLU
  2. Bryant et al's Deciding CLU
  3. Malik et al's Chaff SAT solver (to be handed out in class)

• 3/20/2004: I installed a new version of ACL2. The Tools page has been updated to point to the new version.
• 2/23/2004: I moved offices. I am now in CCB 217.