Resumen Técnico: CONVER – Uso de Contratos y Síntesis de Invariantes de Bucle para la Verificación Formal Escalable de Software

Enunciado del Problema

La verificación formal de programas C a gran escala se ve actualmente obstaculizada por el problema de la explosión del espacio de estados. Las herramientas de Verificación de Modelos Acotados (BMC), como ESBMC y CBMC, deben desenrollar todas las construcciones anidadas (bucles y llamadas a funciones) hasta un límite predeterminado para codificar el espacio de estados como una fórmula SMT. A medida que aumenta el tamaño del programa, el número de funciones y las profundidades de llamada provocan que la instancia SMT crezca rápidamente, haciendo que la verificación sea intratable. Aunque los contratos de función son una técnica de mitigación estándar para abstraer los internos de las funciones, la creación manual de estos contratos requiere expertos y rara vez se adopta en la práctica, limitando la verificación formal a programas de solo unas pocas cientos de líneas.

Metodología

CONVER es una herramienta de verificación composicional de arriba hacia abajo diseñada para automatizar la derivación de contratos de función e invariantes de bucle utilizando Modelos de Lenguaje Grandes (LLM). Opera dentro de un bucle CEGAR-CEGIS (Refinamiento de Abstracción Guiado por Contrajemplo / Síntesis Inductiva), utilizando ESBMC como motor de verificación subyacente.

Flujo de Trabajo Principal

1. Descomposición de Arriba hacia Abajo: En lugar de comenzar con especificaciones de funciones individuales, CONVER comienza con una aserción de sistema de nivel superior en main(). Un LLM sintetiza contratos de función iniciales (precondiciones, postcondiciones y cláusulas assigns) suficientes para probar esta propiedad del sistema.
2. Verificación de Dos Niveles:
   • Nivel de Sistema: Las llamadas a funciones se reemplazan con stubs de contrato abstractos. ESBMC verifica si la propiedad del sistema se cumple asumiendo que los contratos son verdaderos, sin explorar los internos de las funciones.
   • Nivel de Función: La implementación real de cada función se verifica de forma aislada contra su contrato específico.
3. Bucles de Refinamiento:
   • CEGAR con SMART ICE: Si la verificación falla, los contraejemplos se clasifican en ejemplos Positivos (estados que deben incluirse), Negativos (estados que deben excluirse) e de Implicación (relaciones inductivas). Esta retroalimentación estructurada guía al LLM para refinar los contratos. Los fallos a nivel de sistema solicitan contratos más fuertes; los fallos a nivel de función solicitan contratos más débiles (más permisivos).
   • Escalada CEGIS: Si CEGAR se estanca, el sistema escala a una fase de síntesis basada en restricciones. Acumula ejemplos de intentos fallidos para guiar al LLM hacia contratos consistentes con todos los comportamientos observados.
4. Estrategia de Pre-Abstracción: Para funciones con alta complejidad estructural (por ejemplo, recursión profunda, bucles no acotados) que desencadenan explosión de estados incluso a nivel de función, CONVER emplea una fase de pre-abstracción. Genera contratos de sobre-aproximación "laxos" pero sólidos (por ejemplo, seguridad nula, límites de rango) para permitir la verificación inicial, los cuales son reemplazados posteriormente por contratos precisos si la propiedad del sistema se cumple.
5. ESBMC-LF: Un preprocesador especializado que transpila los puntos de referencia Lingua Franca (LF) en programas C monolíticos preservando las propiedades de verificación (fórmulas MTL), permitiendo que CONVER verifique sistemas reactivos complejos originalmente escritos en LF.

Contribuciones Clave

1. Derivación de Contratos de Arriba hacia Abajo: Una metodología que deriva contratos de función directamente desde aserciones de nivel de sistema, minimizando el esfuerzo de especificación manual al centrarse solo en las propiedades requeridas para la prueba del sistema.
2. CEGAR con Aprendizaje SMART ICE: Un bucle de refinamiento iterativo que clasifica los contraejemplos de ESBMC en ejemplos positivos, negativos e de implicación para guiar la re-síntesis dirigida del LLM, mejorando la convergencia sobre el CEGAR estándar.
3. Síntesis de Invariantes de Bucle: Un paso de generación de invariantes inductivos bajo demanda integrado en el bucle CEGIS para funciones donde la verificación acotada es insuficiente.
4. Evaluación de Extremo a Extremo: Un estudio empírico exhaustivo a través de cuatro suites de puntos de referencia que cubren estructuras diversas (algorítmicas, recursivas, con muchos punteros y sistemas reactivos).
5. Preprocesador ESBMC-LF: Una herramienta que permite la verificación de puntos de referencia LF convirtiéndolos a C mientras mantiene las construcciones de verificación, facilitando la verificación de la suite "LF-Hard".

Resultados Experimentales

Los autores evaluaron CONVER en 79 programas C a través de cuatro suites de puntos de referencia utilizando tres backends de LLM (Qwen3.5-Plus, Claude Haiku 4.5 y GPT-OSS 120b):

• Frama-C Benchmark (45 programas): CONVER logró un 82–96% de éxito en la verificación. Cabe destacar que el 93–95% de los programas convergentes requirió solo una iteración de CEGAR. GPT-OSS 120b tuvo el mejor rendimiento (96%).
• LF2C-Simple (17 programas): Logró un 82–88% de éxito, demostrando la capacidad del pipeline para generalizar más allá del punto de referencia principal.
• Analizador X.509 (6 programas): Logró un 33–50% de éxito. La tasa más baja resalta la dificultad de sintetizar contratos de punteros sólidos para operaciones de memoria de bajo nivel con los LLM actuales.
• VerifyThis (11 programas): Utilizando la estrategia de Pre-Abstracción, CONVER logró un 55–64% de éxito. Claude Haiku 4.5 igualó los resultados de referencia de expertos (7/11).
• LF-Hard (24 programas): Estos son traducciones C monolíticas complejas de puntos de referencia LF. La verificación directa con ESBMC tuvo éxito solo en el 42% (10/24). Con la estrategia de Pre-Abstracción de CONVER, las tasas de éxito mejoraron al 46–62%, con GPT-OSS 120b liderando con un 62%.

Estudio de Ablación (RQ2): El estudio encontró que el aprendizaje SMART ICE actúa como un "amplificador de capacidades". Mejoró significativamente los resultados para modelos de alta capacidad (GPT-OSS 120b: +5%, Qwen: +2%), pero degradó el rendimiento para modelos más pequeños (Claude Haiku 4.5: -2%) debido a la acumulación de ruido sintáctico en la base de datos de contraejemplos.

Significado y Afirmaciones

El artículo afirma que CONVER aborda la barrera de escalabilidad en la verificación formal automatizando el aspecto más laborioso: la especificación de contratos. Al combinar la descomposición de arriba hacia abajo con la síntesis impulsada por LLM y la retroalimentación estructurada de contraejemplos, CONVER permite la verificación de programas que de otro modo serían intratables para las herramientas BMC monolíticas.

Los autores enfatizan que el enfoque es sólido porque las decisiones de verificación se delegan al verificador de modelos (ESBMC), no al LLM; el LLM solo propone anotaciones candidatas. Los resultados sugieren que para programas bien estructurados, el bucle CEGAR+ICE es en gran medida agnóstico al modelo, mientras que para programas complejos, con muchos punteros o recursivos, la calidad del backend LLM se convierte en la restricción limitante. El trabajo también demuestra que convertir lenguajes específicos de dominio (como LF) a C mediante herramientas como ESBMC-LF permite que los verificadores C estándar manejen puntos de referencia complejos de sistemas reactivos.

El artículo concluye con modestia, señalando que, aunque el enfoque es efectivo para programas de una sola aserción, se necesita trabajo futuro para manejar programas de múltiples propiedades e investigar estrategias de selección de modelos híbridos. También reconoce las limitaciones relacionadas con la incapacidad actual de ESBMC para verificar mecánicamente las condiciones de marco para los objetivos de desreferencia de punteros.