Course Description:

The area of formal methods consists of a collection of theoretical tools and algorithms to mathematically reason about computation. Formal methods include models of computation such as nondeterministic and probabilistic state machines, automata representing finite or infinite computation, and dynamical system models where computation evolves either in discrete time steps, in continuous time, or in a hybrid fashion. To reason about properties of system behaviors, we often use different kinds of temporal logics and automata. The use of formal methods allows us to rigorously define analysis problems such as: the verification problem (do all system behaviors satisfy a desired property?), the synthesis problem (does there exist a controller/strategy/policy that ensures that the system always exhibits desired behavior?), and the testing/debugging problem (does the system exhibit failure of a specific desired property?) There is a long standing tradition of applying techniques from the formal methods domain to analyze robotic systems. In this course, we will read and discuss important papers in the formal methods domain as well as the robotics domain. We will particularly focus on the papers where there is some intersection between these two areas.

This course has a special focus on paper writing, reading and reviewing. Each student will produce a term paper at the end of the course. In the ideal scenario, this paper would be ready for submission at a top notch robotics or formal methods conference. We will simulate a peer review system where students will review each others' papers. The reviews themselves will be graded, so writing a good review will be an important part of this class.