Resumo Técnico: CONVER – Usando Contratos e Síntese de Invariantes de Loop para Verificação Formal Escalável de Software

Declaração do Problema

A verificação formal de programas C em grande escala é atualmente prejudicada pelo problema da explosão do espaço de estados. Ferramentas de Verificação de Modelo Limitado (BMC), como ESBMC e CBMC, devem desenrolar todas as estruturas aninhadas (loops e chamadas de função) até um limite predeterminado para codificar o espaço de estados como uma fórmula SMT. À medida que o tamanho do programa aumenta, o número de funções e profundidades de chamada faz com que a instância SMT cresça rapidamente, tornando a verificação intratável. Embora contratos de função sejam uma técnica padrão de mitigação para abstrair os internals de funções, a criação manual desses contratos é intensiva em especialistas e raramente adotada na prática, limitando a verificação formal a programas de apenas algumas centenas de linhas.

Metodologia

CONVER é uma ferramenta de verificação composicional de cima para baixo projetada para automatizar a derivação de contratos de função e invariantes de loop usando Modelos de Linguagem Grandes (LLMs). Ela opera dentro de um loop CEGAR-CEGIS (Refinamento de Abstração Guiado por Contraexemplo / Síntese Indutiva), utilizando o ESBMC como motor de verificação subjacente.

Fluxo de Trabalho Principal

1. Decomposição de Cima para Baixo: Em vez de começar com especificações de funções individuais, o CONVER começa com uma asserção de sistema de nível superior em main(). Um LLM sintetiza contratos de função iniciais (pré-condições, pós-condições e cláusulas assigns) suficientes para provar essa propriedade do sistema.
2. Verificação em Dois Níveis:
   • Nível de Sistema: As chamadas de função são substituídas por stubs de contrato abstratos. O ESBMC verifica se a propriedade do sistema se mantém assumindo que os contratos são verdadeiros, sem explorar os internals da função.
   • Nível de Função: A implementação real de cada função é verificada isoladamente contra seu contrato específico.
3. Loops de Refinamento:
   • CEGAR com SMART ICE: Se a verificação falhar, os contraexemplos são classificados em exemplos Positivos (estados que devem ser incluídos), Negativos (estados que devem ser excluídos) e de Implicação (relações indutivas). Esse feedback estruturado guia o LLM a refinar os contratos. Falhas no nível do sistema solicitam contratos mais fortes; falhas no nível da função solicitam contratos mais fracos (mais permissivos).
   • Escalonamento CEGIS: Se o CEGAR estagnar, o sistema escala para uma fase de síntese baseada em restrições. Ele acumula exemplos de tentativas falhas para guiar o LLM em direção a contratos consistentes com todos os comportamentos observados.
4. Estratégia de Pré-Absorção: Para funções com alta complexidade estrutural (por exemplo, recursão profunda, loops ilimitados) que desencadeiam explosão de estados mesmo no nível da função, o CONVER emprega uma fase de pré-abstração. Ele gera contratos de super-approximação "soltos" mas corretos (por exemplo, segurança de nulo, limites de intervalo) para permitir a verificação inicial, que são posteriormente substituídos por contratos precisos se a propriedade do sistema se mantiver.
5. ESBMC-LF: Um pré-processador especializado que transpila benchmarks Lingua Franca (LF) em programas C monolíticos, preservando propriedades de verificação (fórmulas MTL), permitindo que o CONVER verifique sistemas reativos complexos originalmente escritos em LF.

Contribuições Principais

1. Derivação de Contratos de Cima para Baixo: Uma metodologia que deriva contratos de função diretamente de asserções de nível de sistema, minimizando o esforço de especificação manual ao focar apenas nas propriedades necessárias para a prova do sistema.
2. CEGAR com Aprendizado SMART ICE: Um loop de refinamento iterativo que classifica contraexemplos do ESBMC em exemplos positivos, negativos e de implicação para guiar a re-síntese direcionada do LLM, melhorando a convergência em relação ao CEGAR padrão.
3. Síntese de Invariantes de Loop: Uma etapa de geração de invariantes indutivos sob demanda integrada ao loop CEGIS para funções onde a verificação limitada é insuficiente.
4. Avaliação de Ponta a Ponta: Um estudo empírico abrangente em quatro conjuntos de benchmarks cobrindo estruturas diversas (algorítmicas, recursivas, ricas em ponteiros e sistemas reativos).
5. Pré-processador ESBMC-LF: Uma ferramenta que permite a verificação de benchmarks LF convertendo-os para C enquanto mantém construções de verificação, facilitando a verificação do conjunto "LF-Difícil".

Resultados Experimentais

Os autores avaliaram o CONVER em 79 programas C em quatro conjuntos de benchmarks usando três backends de LLM (Qwen3.5-Plus, Claude Haiku 4.5 e GPT-OSS 120b):

• Benchmark Frama-C (45 programas): O CONVER alcançou 82–96% de sucesso na verificação. Notavelmente, 93–95% dos programas convergidos exigiram apenas uma única iteração CEGAR. O GPT-OSS 120b teve o melhor desempenho (96%).
• LF2C-Simple (17 programas): Alcançou 82–88% de sucesso, demonstrando a capacidade do pipeline de generalizar além do benchmark principal.
• Parser X.509 (6 programas): Alcançou 33–50% de sucesso. A taxa mais baixa destaca a dificuldade de sintetizar contratos de ponteiro corretos para operações de memória de baixo nível com LLMs atuais.
• VerifyThis (11 programas): Usando a estratégia de Pré-Absorção, o CONVER alcançou 55–64% de sucesso. O Claude Haiku 4.5 igualou os resultados de referência de especialistas (7/11).
• LF-Difícil (24 programas): Estes são traduções C monolíticas complexas de benchmarks LF. A verificação direta do ESBMC teve sucesso em apenas 42% (10/24). Com a estratégia de Pré-Absorção do CONVER, as taxas de sucesso melhoraram para 46–62%, com o GPT-OSS 120b liderando em 62%.

Estudo de Ablação (RQ2): O estudo constatou que o aprendizado SMART ICE atua como um "amplificador de capacidade". Melhorou significativamente os resultados para modelos de alta capacidade (GPT-OSS 120b: +5%, Qwen: +2%), mas degradou o desempenho para modelos menores (Claude Haiku 4.5: -2%) devido ao acúmulo de ruído sintético no banco de dados de contraexemplos.

Significado e Alegações

O artigo afirma que o CONVER aborda a barreira de escalabilidade na verificação formal automatizando o aspecto mais trabalhoso: a especificação de contratos. Ao combinar decomposição de cima para baixo com síntese orientada por LLM e feedback estruturado de contraexemplos, o CONVER permite a verificação de programas que são de outra forma intratáveis para ferramentas BMC monolíticas.

Os autores enfatizam que a abordagem é correta porque as decisões de verificação são delegadas ao verificador de modelo (ESBMC), não ao LLM; o LLM apenas propõe anotações candidatas. Os resultados sugerem que, para programas bem estruturados, o loop CEGAR+ICE é em grande parte agnóstico ao modelo, enquanto, para programas complexos, ricos em ponteiros ou recursivos, a qualidade do backend do LLM torna-se a restrição limitante. O trabalho também demonstra que converter linguagens de domínio específico (como LF) para C por meio de ferramentas como o ESBMC-LF permite que verificadores C padrão lidem com benchmarks complexos de sistemas reativos.

O artigo conclui com modéstia, observando que, embora a abordagem seja eficaz para programas de asserção única, trabalhos futuros são necessários para lidar com programas de múltiplas propriedades e investigar estratégias de seleção de modelos híbridos. Também reconhece limitações relacionadas à incapacidade atual do ESBMC de verificar mecanicamente condições de quadro para alvos de desreferenciação de ponteiros.