EECS 219C: Computer-Aided Verification

(Model Checking and Computational Logic)

Spring 2006

General Information

• Instructor: Sanjit A. Seshia (office: Cory 568)
• Class Hours: Monday-Wednesday 10 - 11:30 am, in 531 Cory
• Office Hours: Wed. 11:30 am - 12:30 pm, in 568 Cory
• Credits: 3 units

• Homeworks: (50%) There will be 6 homework assignments, with a new one assigned approximately every other week. Each assignment will be worth 10% of the grade, and can include both theoretical problems and experimentation with verification tools. Each student must sign up to help grade one of the assignments, which he/she can drop. The 5 highest homework scores will count. Homeworks will be due at the beginning of class, a 20% late penalty will apply otherwise.

  See here for a what grading a homework involves and the grading schedule.

• Project: (50%) The course project must be a theoretical and/or experimental investigation into the use of model checking or other techniques in computational logic into problems in verification, synthesis, planning, etc. Potential project topics will be announced in the first two weeks of the semester (click here). It is expected that students team up in groups of 2 or 3 for their project. Projects will culminate in a final paper, presentation, and possibly a demo.
• Teamwork: Students may collaborate on homeworks, but each student must individually write up his or her solutions and be prepared to present it in class on the due date. Indicate on your homework the names of those you have collaborated with and on which problems.

Here is a list of suggested projects (Berkeley campus access only).

Here is the project schedule.

Anticipated Topics and Schedule

• The SPIN model checker
• The NuSMV model checker