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.
Prerequisites
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.
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.