15-398 Assignments, Exams and Solutions
 
Assignment Date Assigned Date Due Link to Solutions
Homework 1:Parser Readme   09/23/01  
Homework 2 (ps) (pdf)  09/19/02 10/07/02  
Homework 3 (ps) (pdf)  10/10/02 10/29/02  
Homework 4 (ps) (pdf)  11/07/02 11/22/02  
Homework 5  11/07/02 12/03/02  
Final Project (optional) (ps) (pdf)  11/19/02 12/05/02  

Typed homework is not required, but we don't discourage it. It is your responsibility to make sure your handin is legible. If you want to use LaTeX, use the Sample LaTeX Template. The postscript version of this template is Postscript Sample. You are also welcome to use WORD.


SPIN and XSPIN

I have installed SPIN and XSPIN in:
	    /afs/andrew/usr/flerda/classes/15-398/bin
			    

SMV and NuSMV

I have installed SMV and NuSMV in:
	    /afs/andrew/usr/flerda/classes/15-398/bin
			    
If you add that directory to your path it should run.
In it there are: You are encouraged to try them (I run them on a few examples on a machine of the linux.andrew.cmu.edu cluster and they seems to work) and let me know if anything does not run properly.

Here are some links where you can find more information and download the tools themselves.

SMV
Official Website: http://www-2.cs.cmu.edu/~modelcheck/smv.html
Here you can find the source code for UNIX and an executable for Windows NT. I will soon test the NT version to see if it works correctly on other versions of Windows. It also contains links to binaries for some UNIX including Linux.
NuSMV
Official Website: http://nusmv.itc.it/
There are binaries and source distribution for NuSMV as well as documentation.