15-817 Introduction to Model Checking - Assignments and Exams

Assignment Date Assigned Date Due

Homework 1 (LaTeX source)
cudd-assignment.cc

• The file cudd-assignment.cc has been updated (as of Oct 1 at 23:59) to include sample code for writing a DOT file.
• (削除) Suggestion: Use bdd-asgn1.c instead of cudd-assignment.cc if you're having trouble creating DOT output files. (削除ここまで)
• See the announcements on the main page for a note concerning compiling CUDD with the 64-version of gcc.
• If you can't get GraphViz to work, submit a printout of the source code that you wrote instead, and draw the OBDDs by hand.
• You can download CUDD from here: ftp://vlsi.colorado.edu/pub/cudd-2.4.2.tar.gz

09/24 Probs 1, 2, 3, 4(a): Due Oct 1

Prob 4(b) and bonus: Oct 15

Homework 2 (LaTeX source)

• "~g U ~f & ~g" means "~g U (~f & ~g)"
• If you're stuck on the hint in for 4(c), try drawing a few timelines showing the values of f and g. This should give you insight into why the two sides of the equation must be equal.

10/01 10/08

Homework 3a, Homework 3b (LaTeX source)

• For Assignment 3b, you only need to prove the weaker version ({z | T(z) ⊆ z} instead of {z | T(z) = z}}.
• Proof of Tarski's Fixed-Point Lemma: See the readings page.
• For Exercise 3(d), [π^0 |= ack] is a "don't care". That is, the property in 3(d) is unaffected by whether ack holds true on the initial state of the path.

  Does it make sense for ack to hold true on the initial state
  of path $\pi$? If we consider another path $\pi_b,ドル and $\pi$
  is a suffix of $\pi_b,ドル so that $\pi = \pi_b^k$ for some $k,ドル
  and $\pi_b^{k-1} \models \req,ドル then it would make sense for
  $\pi^0 \models \ack$ to hold true.
  

• Homework 3 is now split into two parts, 3a and 3b.
• Also due Oct 15: Homework 1 Problem 4(b) and the Bonus problem. Both of these are now bonus problems.

10/08 10/15

Homework 4 (LaTeX source)
simple-01.smv

• Read pages 1--4 of the original SMV manual.
• It may be helpful to look at the Microwave example and the Simple01 example from the previous year's lecture on SMV.
• Hint for Exercise 2: Write an expression that gives the possible next values of each variable (a, b, c, d) in terms of their current values.
• Cadence SMV can be downloaded here: http://www.kenmcmil.com/smv.html
• Running Cadence SMV on the CMU Andrew machines

10/15 10/22

No homework this week. 10/22 10/29

Homework 5 (LaTeX source)

• For Exercise 2, assume that State 1 (the topmost state) is the start state.
• For an LTL path formula f, treat it as a CTL* formula [A f]; this is the convention that SMV uses.
• Depending on how you write your SMV files, there may be issues getting SMV to accept the LTL formulas; if this is the case, just do the analysis by hand and show your work.

10/29 11/05

Homework 6 (LaTeX source) 11/05 11/19