NuSMV, a model-checker [documentation | download]
NuSMV is installed on both CS and CCC (executable is ~kfisler/VerifTools/nusmv-1.1/NuSMV on both systems). You can also download it on your home machine if you wish. It should install fairly easily on Unix/Linux systems. I can't make any guarantees about Windows (some people have gotten it to work; I'm still debugging my Windows installation).
If you can't get NuSMV to install on your Windows platform, use Cadence-SMV. It's source-compatible with the SMV constructs we've used so far (and expect to use through the course).
ACL2, a theorem prover
Course grades will be based on the following activities:
| Assignment | Percentage |
|---|---|
| Paper Summaries | 15% |
| Homework Exercises | 40% |
| Final Project | 35% |
| Class Participation | 10% |
There are no exams in the course.
Late policy: Assignments (exercises and paper summaries) are due on the date specified on the assignment handout. Assignments may be turned in up to one day (24 hours) late, for a 20% penalty. Assignments will not be accepted beyond one day late without prior arrangement or an emergency situation.
Collaboration policy: Each assignment handout will contain a clearly-stated collaboration policy. You are free to discuss assignments with other students within the constraints of the policy. If you have questions about the policy for a particular assignment, ask! Violations of the collaboration policy generally result in an NR or F for the course. Your only chance to avoid an NR or F is to admit the violation to me before I detect it.
|
This page maintained by Kathi Fisler Department of Computer Science Worcester Polytechnic Institute |