Logic Model Checking, Caltech 2013, Winter Term


Course Material CS 118, TThu, 1:00-2:25pm, 314 Annenberg


Logic Model Checking

This course offers an introduction to the theory and practice of logic model checking as an aid in the formal verification of concurrent and multi-threaded software systems. The specific focus is on the automata-theoretic verification method, on the formalization of properties in linear temporal logic, and the use of the Spin model checker. The course also covers automated model-extraction and swarm-based verification techniques using grid networks, the cloud, and standard multi-core machines.

At the end of the course you should have a good fundamental insight into the theory of logic model checking based on automata-theoretic verification, and the direction in which the research in this area is evolving. At that point you should be able to handle significant real-world software verification problems, especially of systems involving concurrency.

Assignments:
There are seven take-home assignment, roughly one per week, and especially in the beginning a fair amount of self-paced work with Spin is expected. Some of the assignments will require significant effort, formalizing problems and finding abstractions to make verification tractable.

The first five assignments each count for 10% of the final grade; the last two assignments each count for 25%.
The maximum score for each assignment is 100 points. If you send in your solution past the due date/time, 10 points are deducted for every 24 hour period or part thereof. (I.e., at the start of the 10th day late, zero points will remain.)

A letter grade for the course is derived from the following ranges for the weighted average score on all assignments:

	95 - 100  = A+
	85 - 94   = A
	80 - 84   = B+
	70 - 80   = B
	65 - 69   = C+
	55 - 64   = C
Examples of assignments and small model checking applications will be discussed during each lecture, so you are strongly encouraged to attend in person. It is possible that some assignments are done only in class this year, which can gain you additional credits towards the final grade.

Labtime/Homework:
At the start of the course you are expected to download and install the latest version of Spin model checker on your preferred system (linux recommended). Throughout the course you are further expected to take the initiative to experiment on your own with the tool to learn in more detail about concepts explained in the lectures, and to ask questions based on these experiments.
You are strongly encouraged to try small examples to develop and fine-tune your model building, abstraction, and verification skills, and to develop insight in the verification strategies that are typically used with logic model checkers. Self-paced work is expected throughout the course.

Lectures

Assignments and Exercises

Exercises

  • by January 8, 2013:
  • by January 15, 2013:
  • by February 5, 2013:
  • Last 3 Lectures:
    • March 5: Model Checking with Bounded Context Switching
    • March 7: Multi-Core Depth-First and Breadth-First Search
    • March 12: Swarm Verification Techniques (using Grid/Cloud Networks)

    Assignments

    #posteddue@noonpdf
    1January 15 Tuesday January 22 pdf
    2January 22 Tuesday January 29 pdf
    3January 29 Tuesday February 5 pdf
    4February 5 Tuesday February 14 pdf
    5February 19Tuesday February 26 pdf
    6February 26Wednesday March 6 pdf
    7March 5 Thursday March 14 pdf

    Instructor

    Teaching Assistant

    Course Website

    Background material

    Course Textbook

    Required:

    Optional:

    For more on mutual exclusion algorithms, and design of distributed algorithms in general, consider also:


    Spin homepage