Ponente: Lourdes del Carmen González Huesca
Institución: FC-UNAM
06/05/2025 de 12:00 a 13:00
Dónde Auditorio "Alfonso Nápoles Gándara"
En esta plática se abordarán las bases que permiten tener lenguajes expresivos para la verificación formal. Por un lado, están las lógicas de orden superior como lenguajes para establecer especificaciones o propiedades a demostrar. Por otro lado, se provee a los lenguajes de programación con tipos refinados que también establecen contratos detallados sobre las propiedades de programas. Estos todos aspectos definen a la correspondencia entre lógica y programas, parte fundamental de la verificación formal.