Winter 2007: CSE 291 - Model Checking







Course Description

Model checking concerns the use of algorithmic methods in the temporal safety and performance assurance for software and hardware systems. As our daily lives depend increasingly on digital systems, the reliability of these systems becomes a concern of overwhelming importance, and as the complexity of the systems grows, their reliability can no longer be sufficiently controlled by the traditional approaches of testing and simulation. Model checking techniques have been successfully applied to a variety of systems including hardware circuits, network protocols, cryptographic protocols, distributed systems, device drivers, OS kernels, file systems, network switches, web services. At UCSD alone, members of the embedded systems, databases, sysnet, security and PL/SE groups are working on applications of model checking to their respective domains. In this class we will see the theoretical foundations, basic algorithmic techniques, and recent advances and connections with static and dynamic program analysis, together with case studies on how model checking has been applied to various domains. The topics we will cover include: Temporal Logic, Enumerative verification, Model Reduction, Symbolic algorithms, Automatic Abstraction and Refinement, Shape Analysis and Dynamic Model Checking.


The class will be mainly self-contained. Familiarity with undergrad level Data Structures, Algorithms, Computability and Complexity Theory, Programming Languages, Compilers and Operating Systems will be useful. For example, you should know what a tautology is, how to determinize a finite automaton, what PSPACE stands for, and how to find the strongly connected components of a graph. If you are not familiar with these concepts, please see the instructor.


Lecture notes will be handed out. We will occasionally, refer to: Clarke, Grumberg, and Peled, Model Checking, MIT Press.

Requirements and Grading


Potential project topics, both theoretical and experimental, will be announced during the first weeks of the course. Any suggestions for designing your own project according to your interests are very welcome. Every project will require a mentor. Projects will involve either surveying a field in depth, or using state of the art model checkers to verify large systems of interest, or to extend the capabilities of existing model checkers by implementing new algorithms or proving new theorems. The project can be counted for both this class and CSE 230.