GECO - Verificación gradual e ingeniería de prueba robusta para COq

El equipo asociado GECO está liderado por Nicolas Tabareau del equipo-proyecto GALLINETTE en Francia y en Chile por Éric Tanter, investigador del Departamento de Ciencias de la Computación (DCC) de la Universidad de Chile. Buscando aportar mejoras significativas al asistente de pruebas Coq, el equipo reúne a investigadores de Inria y de distintas instituciones en Chile (Inria Chile y Universidad de Chile).

El enfoque de este proyecto es tanto teórico como práctico, cubriendo fundamentos y métodos novedosos, diseño de lenguajes y herramientas concretas y validación a través de estudios de casos específicos. El resultado final será una serie de mejoras en el asistente de pruebas de Coq (marcos, lenguaje táctico) junto con pautas y demostraciones de su aplicabilidad en escenarios realistas.