Aprender a manejar a uno de los métodos formales más potentes que es model checking. En principio, model checking es trivial: simplemente generar todos posibles estados de un programa y verificar que las especificaciones de corrección se mantienen en cada estado. En el curso se usará model checker Spin para modelar y verificar sistemas concurrentes. Modelos en Spin se escriben en el lenguaje Promela.