Department of Computer Science
CPSC 513: Introduction to Formal Verification and Analysis


Assignments:

Assignment 1: (Assigned September 13, Due September 25)

Fill in some missing code to get a working combinational circuit comparison tool using BDDs. Please finish before class time on September 25, so we can talk about the assignment in class. Also, start early! The assignment should be very easy, once you get the hang of things, but the initial learning curve can be steep.

Assignment 2: (Assigned September 25, Due October 4)

Fill in some missing code to get a working combinational circuit comparison tool using SAT. I normally always ask that you please handin your assignment before class time, so we can talk about it if anyone wants. However, Sam Bayless will be covering my lectures that day, so I won't be strict about the deadline. The deadline is mainly because we need to keep moving with the next little assignment...

Assignment 3: (Assigned October 11, NEW! By popular acquiescence, the due date is Wednesday, October 18! Due October 23)

Write a simple sorting program and then generate the SMT expressions to verify that the output is sorted. Detailed description of assignment.

Assignment 4: (Assigned Oct 18, Due Oct 25)

Use Murphi to model and verify a simple cache coherence protocol. Link to description of assignment.

Choose one (or both) of 5a or 5b!

5a is better if you think you'll be implementing something with BDDs for your project. 5b is better if you think you'll be using a model checking tool to verify something.

Assignment 5a: (Assigned October 25, Due November 1NEW! Extended to November 6))

Fill in some missing code to get a working (BDD-based symbolic) reachability program for sequential circuits. Link to description of assignment.

Assignment 5b: (Assigned October 25, Due November 1NEW! Extended to November 6))

Add some specs and fairness constraints to verify (or find errors in) a simple mutual exclusion protocol. Link to description of assignment.