CS 685, Special Topics in Computer Science: Model Checking

Instructor: Dr. Victor W. Marek
Time: 9:00-9:50, MWF (it is now official)
255 FPAT
Office: 779 FPAT (Anderson Hall)
Office hours: 3:00-3:50, MWF and by appointment
Phone: (859) 257-3496
email: marek@cs.uky.edu.

Handbook: M. Huth and M. Ryan "Logic in Computer Science", ISBN 0 521 54310 X, but I will also use G.L. Gopalakrishnan "Computation Engineering, Applied Automata Theory and Logic" ISBN 0-387-24418-2 (but international editions may have different ISBN). Notes by the instructor will be available. I will not teach anything that will be not in the notes.

Here are the topics:

  1. Symbolic techniques: BDD, Clausal Logic, (satisfiability algorithms and ROBDD manipulation algorithms)
  2. Refresher of Automata Theory
  3. Basics of model checking
  4. Temporal logic
  5. Algorithms for model checking

Detailed topics (per day of classes) can be hound on this page. I will update this page (hopefully) immediately after class.

Since this is a topics graduate course the students are expected to take active part in the course. Some elements of involvement will require use of specific software related to Model Checking. Depending on the enrollment in the course, students will be working in groups or individually (working individually will always be an option) preparing presentation of a specific piece of software related to Model Checking. Here are some of the software I have in mind: zchaff, aspps, alloy, NuSVM, and possibly other software. Student or a group of students will have to:

  1. Bring and compile the software
  2. Explain what this software can do
  3. Explain what role that software plays in tasks associated with Model checking

Expected outcomes of the course. By the end of the course the student will understand fundamental issues of Model Checking These include:

  1. The purpose of Model Checking
  2. The use of symbolic techniques
  3. Temporal logic LTL
  4. Use of tools such as SAT and BDD for model checking

Understanding of these issues, primarily related to the more advanced areas of applied logic is the fundamental goal of this course.

The credit for this course will be determined as follows:

Grading Scale:

Homeworks will be posted via homeworks page. There should be 6 or 7 homeworks, every other week. Homeworks should, in principle, correspond to the topics outlined above. The homeworks page will be up during the second week of classes.

I will negotiate with students (groups of students) the topic of the project, that is the specific software they will present. The presentation will consists of discussing some theoretical underpinnings of the software, and the presentation of the software in action. I will work with the groups to help them make a meaningful presentation.

There will be class mailing list. I will announce posting of homeworks and tests on that list.

Students can communicate with me through e-mail (marek@cs.uky.edu). Please do not expect the instantaneous answer esp. during weekends. I try to cut reading mail on weekends. Normally, I read my mail both during my working hours and also evening hours.

Attendance: I will check attendance at least once a week.

Final Remarks

  1. Cheating and Plagiarism will be pursued if they occur. See Student's Rights and Responsibilities for applicable penalties.
  2. Group work on homeworks and the project is not acceptable.
  3. Students with appointments always have priority over those without appointments, even during office hours. I encourage questions be email.
  4. I discourage eating, drinking, and other types of distracting behavior during my classes (but drinking pure water is, in my view an acceptable activity). Reading newspapers, solving problems for other lectures etc. should not take place in the classroom. Wearing baseball hats in class, backwards, is strongly discouraged. The instructor never wears the hat backwards.

Set up: 27/03/08

Last modified: 13/07/08