Introducción a la Verificación Formal

Dictado 2025

Repositorio de la materia: https://github.com/mtzguido/intro-verif-25

Materias previas: ALP. MUY recomendadas: Ingeniería de Software 1, Seguridad Informática.

Libro: ★ PDF ★ Interactivo ★ PDF estático (copiado 26/08/2025)

Clases

#	Fecha	Tema	Diapositivas	Material
1	28/08	Introducción a verificación, F*, tipos refinados.	[pdf]	Clase01.fst
2	04/09	Tipos dependientes, lógica formal, Curry-Howard.	[pdf]	Clase02.fst
3	11/09	Recursión, terminación, tipos inductivos (índices, parámetros, GADTS), positividad.	[pdf]	Clase03.GADT.fst Clase03.Positividad.fst Clase03.Recursion.fst Clase03.Vec.fst
4	18/09	Más tipos indexados, pruebas extrínsecas.	[pdf]	Clase04.BST.fst Clase04.Fib.fst Clase04.Listas.fst Clase04.MiniLang.fst

Bibliografía

Requerida

• Proof-Oriented Programming in F*, capítulos 1-4, 6-8, 29 (por ahora)
• Hoare - An axiomatic basis for computer programming (1969)

Complementaria

• Métodos formales en la práctica
  • Reid et al - Towards making formal methods normal: meeting developers where they are (2020)
  • AWS re:Inforce 2024 - Proving the correctness of AWS authorization (IAM401)
• Bugs famosos
  • Bug FDIV del Pentium
  • Vuelo Arianne V88
  • Heartbleed: filtración de datos en OpenSSL
  • Maleabilidad en Bitcoin, y Hackeo a MtGox
  • Spectre y Meltdown: bugs de hardware relacionados a ejecución especulativa
  • Casa Blanca EE.UU. - Back to the Building Blocks: A Path Toward Secure and Measurable Software (2024)
• Verificación
  • Dijkstra - Guarded commands, nondeterminacy and formal derivation of programs (1975)
• Lenguajes de Programación
  • Wadler - Theorems for free! (1989): parametricidad y teoremas gratis
  • Wadler - Propositions as types (2015): correspondencia Curry-Howard
  • Augustsson - Cayenne - a language with dependent types (1998)
  • McBride - Faking it: Simulating dependent types in Haskell (2002)
• Verificación de programas con efectos
  • Dijkstra Monads for Free (2017)
  • Dijkstra Monads for All (2019)
• Verificando verificadores
  • MetaCoq
  • Strub et al - Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq (2012)
  • Andrici, Ciobâcă - A Verified Implementation of the DPLL Algorithm in Dafny (2022)

Proyectos

• Usando F*
  • HACL*: criptografía verificada
  • EverParse: parsers verificados para formatos de red
• Otros proyectos importantes
  • Mathlib de Lean4
  • CompCert: compilador de C verificado
  • sel4: microkernel
  • DeepSpec: especificaciones profundas full-stack
  • Z3: SMT solver (GitHub)
• Sobre Lean:
  • Kevin Buzzard - The Future of Mathematics?
  • Kevin Buzzard - What Computers Can’t Do