Home > Teaching > CS 638: Formal Methods in Robotics and Automation

CS 638: Formal Methods in Robotics and Automation

Units: 3-0-0-9

The term "formal methods" refers to mathematical techniques for verification and automatic synthesis of systems to ensure that the systems satisfy desirable properties given as specification. Formal methods are essential for building systems used for life-critical and mission critical applications. As robots are increasingly being used for such applications, use of formal methods has become critical for building robotic systems. In this course, we will study the recent development of formal methods based techniques for building software for robots. The course will cover basic concepts in formal methods and control theory and illustrate the potential of such techniques to be effective in the development of high quality robotic software.


The course does not have any formal prerequisites. The students are expected to have mathematical maturity of the level of an undergraduate degree in engineering. However, some familiarity with finite state machines and ordinary differential equations, and programming experience will be helpful.

Course Contents:
Books and References:
  1. C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008.
  2. E. M. Clarke, Jr., O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.
  3. K. J. Astrom and R. M. Murray. Feedback Systems: An Introduction for Scientists and Engineers. Prince- ton University Press, 2009. http://www.cds.caltech.edu/~murray/amwiki/index.php/Main_Page.
  4. S. M. LaValle. Planning Algorithms. Cambridge University Press, 2006.
  5.  Relevant research papers.