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. Please finish before class time on October 4, so we can talk about the assignment in class. Also, start early! As before, the assignment should be very easy, once you get the hang of things.

Assignment 3: (Assigned October 4, Due October 16)

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 16, Due Oct 25)

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

Optional Assignment 5: (Assigned Nov 8, Due Nov 30)

As discussed in class, this is something it's a real pity to miss out on, but I'd rather you spend more time on your projects if you can't find time to do both. Nico asked for it to be due at the end of term, and I agreed to a 2-week deadline, but that's basically end-of-term anyway, so I made it due Nov 30.

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

Project: (Presentations Nov 27 and 29; Write-Up Due Dec 19)