CIS 6930/CIS 4930 - AUTOMATED VERIFICATION

Model checking is a verification/validation technique that has emerged as an alternative to traditional techniques such as testing. Although, testing is still the most popular verification technique in the industry, model checking has a bright future as prestigious research labs (Microsoft Research, NASA Ames, Bell Labs, etc) have already developed their in-house model checkers and experimenting with them. The main advantages of model checking are: 1) It can be automated, 2) It is an exhaustive technique, e.g., can show absence of errors, 3) It can provide an explanation (a counter-example) for the source of the bug if there is any. Model checking has been successfully applied to hardware and software verification. Recently, it has been applied to biological pathway analysis. In this course, we'll focus on software verification, however, case studies on application of model checking to other areas are also welcome.

Homeworks (25%): Hands-on experience with model checking tools.
A take-home final exam (25%). (You will pick up the exam on 04/27/07 and submit your solutions on 04/30/07 by 5 pm)
Project (50%): Each student will choose one of the following project types:

Case Study: The student will choose a fairly complex design/program and analyze the correctness properties using at least one model checking tool.

Survey: The student will choose a set of related papers on a specific topic related to model checking and write a survey paper based on these papers. Here is a starting point, you are encouraged to search for more papers on model checking.

Tool extension: The student will improve an existing model checking tool for a certain aspect. This type of project is recommended if the student is interested in model checking research.