Assignments

This course was originally desgined with 4 assignemnts, one for each major topic in the course. The design philosophy behind them was to help cement the understading of each topic. These were group assignments, with the idea that a group of students work together to get these done, by the end, they can be more confident that they have the practical understanding of the topic as the course intended.

Unfotunately, the assignments cannot be made AI-proof. In fact, they are quite the opposite. Those involving solvers are the easiest things for the agents to do, because the agents can use the verifiers to check their work. Ironically, this precisely the point of this course: we need formal verificaiton as a complement of agents to get them to deliver the work as intended!

So, I can no longer assign course grade to something that can be done by an agent in minutes. Hence, I will post the assignments here on the normal schedule of the course. If you are interested in learning, you need to do them. Otherwise, you will not learn very little in this course. As an extra incentive, to encourage you to do them, we will have on the exam a question or two that is directly related to the corresponding assignment for the topic . Hence, those who have done the work will get the direct benefit.

The release dates are approximate. Each will be released when the corresponding material is already covered in class.

• Assignment (1): [Program Correctness]
  • Release 9/18
• Assignment (2): [SAT/SMT]
  • Release 10/10
• Assignment (3): [Model Checking]
  • Release 10/30
• Assignment (4): [Dataflow Analysis]
  • Release 11/20