15817 Introduction to Model Checking


Main
Page




Syllabus

Assignments



Grading

Reading


Professor


15817 Assignments, Exams and Solutions
Assignment 
Date Assigned 
Date Due 
Homework 1 (LaTeX source)
cuddassignment.cc
 The file cuddassignment.cc has been updated (as of Oct 1 at 23:59) to include sample code for writing a DOT file.
Suggestion: Use bddasgn1.c instead of cuddassignment.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 64version 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/cudd2.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 FixedPoint 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^{k1} \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)
simple01.smv

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 
