Model checking is an automated approach to the verification of software and hardware systems. This course covers the theoretical foundations of model checking as well as the application of model checking tools to practical problems. Specific topics include transition systems, Kripke structures, temporal logic specification, automata for infinite words, nested depth first search, verification of concurrent algorithms, partial order reduction, the Spin model checker, and symbolic model checking.
Model checking was introduced in 1981 and quickly became a standard tool for verifying the correctness of integrated circuit designs. Shortly thereafter, researchers began extending the approach to verify software. The 2007 Turing Award announcement, reproduced below, provides a nice summary of this history. Today, numerous companies involved in the production of complex software systems---including Microsoft and Amazon, among many others---use model checking as a standard part of their development process. Software engineers with model checking skills work in teams solving some of the most important and interesting problems at these companies. Prospective employees with these skills are always in high demand.
The only prerequisite for the course is CISC 220 (Data Structures) or a similar course. All other necessary background material will be covered in the course itself. The course will largely follow the excellent new text of Clarke et al., which can be purchased in hard copy or electronic form, or rented in electronic form. There will be lectures, practice problems, time for discussion and Q&A, and problem sets. Students will become proficient users of the Spin model checker for verifying the correctness of concurrency protocols and other problems, and will gain a firm understanding of the theoretical underpinnings of model checking.
To register for the course, or if you have any questions at all, email me, Prof. Siegel, email@example.com.
In 1981, Edmund M. Clarke and E. Allen Emerson, working in the USA, and Joseph Sifakis working independently in France, authored seminal papers that founded what has become the highly successful field of Model Checking. This verification technology provides an algorithmic means of determining whether an abstract model--representing, for example, a hardware or software design--satisfies a formal specification expressed as a temporal logic formula. Moreover, if the property does not hold, the method identifies a counterexample execution that shows the source of the problem. The progression of Model Checking to the point where it can be successfully used for complex systems has required the development of sophisticated means of coping with what is known as the state explosion problem. Great strides have been made on this problem over the past 27 years by what is now a very large international research community. As a result many major hardware and software companies are now using Model Checking in practice. Examples of its use include the verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms.
The work of Drs. Clarke, Emerson, and Sifakis continues to be central to the success of this research area. Their work over the years has led to the creation of new logics for specification, new verification algorithms, and surprising theoretical results. Model Checking tools, created by both academic and industrial teams, have resulted in an entirely novel approach to verification and test case generation. This approach, for example, often enables engineers in the electronics industry to design complex systems with considerable assurance regarding the correctness of their initial designs.