En este curso examinaremos la especificación formal de sistemas informáticos, mediante formalismos lógicos y matemáticos que permiten describir con precisión qué debe hacer un producto de software antes de construirlo. Además, se estudiará la estructuración de las descripciones formales y se explorarán maneras en que enfoques de modelaje diagramático y formal pueden complementarse, realizar el refinamiento de especificaciones hacia diseños y programas, aplicar especificaciones al diseño de pruebas, y usar herramientas para examinar las cualidades de las descripciones formales – entre otros.