Profa. Lourdes del Carmen González Huesca lu mi vi 13 a 14 hrs P204
Ayud. Brayan Martínez Santana ma ju 13 a 14 hrs
Evaluación
40 % Tareas
30 % Prácticas
30 % Proyecto Final
Requisitos: Lógica Computacional, Lenguajes de Programación, Autómatas y Leng. Formales, Ingeniería de Software, Semántica y Verificación
Temario
Qué son los Métodos Formales: panorama general, motivación, clasificación y uso.
Para cada uno de los siguientes se revisarán los fundamentos y características principales
QuickCheck
Frama-C
Coq
Referencias
Las referencias principales de cada tema son las siguientes:
O'Regan, Gerard. "Concise Guide to Formal Methods: Theory, Fundamentals and Industry Applications", Springer, 2017.
Nielson, Flemming and Riis Nielson, Hanne. "Formal Methods: An Appetizer", Springer, 2019.
Blanchard, Allan. "Introduction to C program proof with Frama-C and its WP plugin", 2020.
Material
Se proporcionará material complementario como lecturas y resúmenes que se consultan acá.