CS 525V : Introduction to Computer-Aided Verification

Assignment expectations are for students taking the course for credit (as opposed to auditors).

Exercises will be posted here as they become available. I expect to give roughly 4 exercises (outside of the other assignments listed on this page) over the course of the semester.

General Assignment Documentation

• Notes on preparing SMV assignments

Assignment Handouts

• Assignment 1: Modeling and Verifying Simple Designs in SMV.
  Due: Feb 1, 2001, by 6pm. Submit via turnin using assignment name simple-mc.

  Auxiliary files:

  • simplemem.smv
  • itlc.smv
  • A description of the Clayton Tunnel protocol and accident for those of you whose handouts were incomplete.

• Assignment 2: Modeling and Verifying Cache Coherence in SMV [PS, PDF]
  Due: Feb 25, 2001, by 11:59pm. Submit via turnin using assignment name cache.

• Assignment 3: Modeling and Verifying Simple Designs in ACL2
  Due: March 25, 2001, 11:59 pm. Submit via turnin using assignment name simple-acl2.

• Assignment 4: Modeling and Verifying Cache Coherence in ACL2
  Due: April 22, 2001, by 11:59pm. Submit via turnin using assignment name acl2cache.

Each student will present one or two papers in class (depending on final enrollment). The papers will come from the course readings. Your grade on the presentation will be based on the clarity and organization of your presentation and how well you can field questions from your classmates about the paper's contents.

Guidelines for preparing your presentation:

• Examples first! This is the cardinal rule of giving good presentations. Examples motivate the problem and develop intuition about the details coming in the rest of the presentation. Always introduce new concepts through examples.

• Don't just read the paper to the class. Your classmates will have read the paper (though not as carefully as you have). Your job is to effectively present the material in the paper. This often entails presenting the paper's contents in a different order than is written in the paper. Focus on creating a clear presentation (even if the paper authors did not). Aspects of the paper that were not clear to you the first time you read it are likely unclear to others as well, so concentrate on explaining difficult parts of the presentation well.

• Choose your own presentation medium. You may prepare overhead transparencies, a laptop-based presentation, simply use the board, etc. You may prepare handouts for the class if necessary/desired.

• You are welcome (and encouraged) to discuss your presentation with me. We can review an outline, dry-run the presentation, etc. If you've never given a presentation before, I strongly encourage you to review your presentation with me beforehand.

• Some other notes on giving talks. Some of the advice is more for presentations with slides, but the rest is good general advice.

The ability to produce concise technical summaries of other work is an important job skill. Accordingly, each student will produce two paper summaries on course readings (on papers other than ones they present). Each summary should be one page in length and should describe the motivations, contributions, and key ideas of the paper. Also include a brief evaluation of the paper and its utility to other potential readers. Your grade will be based on the accuracy of your summary, the clarity of your summary, and the quality of your writing.

Students are expected to attend class sessions and to participate in class discussions. Asking questions and/or proposing approaches to problems posed in class are good ways to participate in the discussions.

Learning to ask good questions is a useful skill for participating in discussions, both in courses and on the job. To help you learn to ask good questions, students not presenting a paper should come prepared with three questions that they could ask about the paper. You must turn these questions in for feedback until I'm convinced that you know how to develop good questions from reading papers.

Your final project will take one of the following three forms (your choice):

1. Modeling and verification of a substantial design using one of the tools that we discuss in class.

2. Modeling and verification of a reasonable design using a tool that we do not discuss in class. Your project should contrast your experience with the new tool with what you would have expected from verifying the same design in the tools that we used in class.

3. A survey paper (roughly 10-15 pages) describing and contrasting the state-of-the-art approaches to verification in a particular problem domain.

In general, these will be individual projects. However, I will consider team projects provided you propose a project of sufficient scale to warrant multiple team members.

In each case, you will turn in a report describing your project and give a brief presentation on your project to the class at the end of the semester (presentation duration to be determined once I know how many students are enrolled).

You must submit a short project proposal and have me approve it. Proposals will be due sometime mid-semester (date TBA). Start thinking about the kind of project you would like to do. Possible domains include security protocols, e-commerce protocols, graphical-user interfaces, wireless network protocols, particular computer architectures, embedded software systems, etc. I'm glad to help you develop project ideas if you ask.