Sesión 8: Formal Verification and Correctness Listado de artículos correspondientes a la sesión: An Exercise in Proving Red-Black Trees Correct (Trabajo en progreso)Modeling Systems and Proving their Correctness with Event-B and Rodin (Tutorial)A Correct Compiler from Mini-ML to a Big-Step Machine Verified Using Natural Semantics in Coq (Trabajo en progreso)