15-817 Assignments, Exams and Solutions
Assignment Date Assigned Date Due
Homework 1 (LaTeX source)
  • 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)
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