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.
Course WorkHomeworks (40%): Involves hands-on experience
with model checking tools as well as solving problems.
Paper presentation(s) (25%): Each student will choose one or two
papers that have been recently published in top model checking conferences
and give a presentation of the paper in class. The instructor will provide
the list of papers to choose from.
A take-home final exam (35%): The exam will consist of questions that
refer to the papers that will be discussed in class. You will pick up the exam on 04/25/08 and
submit your solutions on 04/28/08 by 5 pm.