🤖 machine learning

Verification Modulo Tested Library Contracts

Este artigo apresenta o framework de verificação "modulo tested library contracts", implementado na ferramenta \vmtlc, que utiliza aprendizado guiado por contraexemplos para sintetizar contratos modulares e contextuais adequados para verificar programas clientes que utilizam bibliotecas complexas.

Autores originais: Abhishek Uppar, Omar Muhammad, Sumanth Prabhu, Deepak D'Souza, Madhusudan P, Adithya Murali

Publicado 2026-04-20

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Abhishek Uppar, Omar Muhammad, Sumanth Prabhu, Deepak D'Souza, Madhusudan P, Adithya Murali

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você é um arquiteto de software (o "cliente") construindo uma casa complexa. Para isso, você precisa usar tijolos, cimento e vigas feitos por uma grande fábrica (a "biblioteca"). O problema é que a fábrica é enorme, cheia de máquinas complexas e ninguém tem tempo de ler todos os manuais de engenharia dela para garantir que cada peça é perfeita.

A verificação tradicional de software tenta ler tudo o que a fábrica faz e provar matematicamente que está tudo certo. Isso é como tentar inspecionar cada tijolo individualmente antes de usar. É exaustivo, lento e, muitas vezes, impossível para fábricas gigantes.

Este artigo apresenta uma solução inteligente e mais prática chamada "Verificação Modulo Contratos Testados". Vamos explicar como funciona usando uma analogia simples:

1. O Problema: A Fábrica Misteriosa

Você quer provar que sua casa (o programa do cliente) não vai desabar. Para isso, você precisa confiar nas vigas (métodos da biblioteca).

O jeito antigo: Você exige que a fábrica prove, com matemática pura, que cada viga é perfeita. Se a fábrica for muito grande, isso nunca acaba.
O jeito novo deste artigo: Em vez de provar matematicamente que a fábrica é perfeita, nós pedimos para a fábrica passar em um teste rigoroso que nós criamos.

2. A Solução: O "Contrato de Confiança"

O sistema funciona como um jogo de "pergunta e resposta" entre três personagens:

O Arquiteto (Seu Programa): Precisa de garantias para construir a casa.
O Detetive (O Testador): Um robô que tenta quebrar as peças da fábrica. Ele joga bolas de basquete, martelos e chutes contra as vigas para ver se elas quebram.
O Tradutor Inteligente (O Síntetizador): É quem cria o "contrato".

Como o jogo funciona:

O Tradutor cria um contrato para a fábrica. Exemplo: "Se você colocar um tijolo vermelho, a viga deve ser forte."
O Detetive tenta quebrar essa viga. Ele tenta colocar um tijolo azul ou verde.
- Se a viga quebrar com um tijolo azul, o Detetive grita: "Ei! O contrato falhou! Você disse que só tijolos vermelhos funcionam, mas eu usei um azul e quebrou!"
- O Tradutor ouve o grito, ajusta o contrato para: "A viga é forte se o tijolo for vermelho OU azul."
Eles repetem isso até que o Detetive não consiga mais quebrar a viga com nenhum teste que ele saiba fazer.
Enquanto isso, o Arquiteto usa esse contrato ajustado para provar que sua casa é segura.

3. A Grande Inovação: "Contratos Contextuais"

Aqui está a parte mais brilhante do artigo.

Contratos Modulares (O jeito chato): O contrato tem que funcionar para qualquer situação no universo. "A viga aguenta qualquer peso, em qualquer lugar, com qualquer cor de tijolo." Isso é muito difícil de provar e de testar.
Contratos Contextuais (O jeito inteligente): O contrato só precisa funcionar dentro da sua casa.
- Analogia: Imagine que você sabe que, na sua casa, você nunca usa tijolos azuis. Você só usa vermelhos.
- Então, o contrato pode ser: "A viga é forte para tijolos vermelhos."
- O Detetive só precisa testar se a viga aguenta tijolos vermelhos. Ele não precisa testar tijolos azuis, porque na sua casa eles nunca aparecem!

Isso torna os contratos muito mais simples, fáceis de criar e mais fáceis de passar no teste. É como dizer: "Não me importa se o elevador funciona se o prédio estiver em chamas; me importa se ele funciona quando o prédio está normal."

4. O "Cérebro" do Sistema (IA e LLMs)

Para criar esses contratos, o sistema usa uma tecnologia chamada ICE Learning. Pense nisso como um aluno que aprende com erros:

Ele tenta uma resposta.
O professor (o verificador) diz: "Errado".
O professor dá um exemplo do que deu errado.
O aluno tenta de novo, aprendendo com o erro.

O artigo também usa Inteligência Artificial (LLMs), como o ChatGPT, para ajudar a adivinhar qual deve ser o contrato inicial. A IA sugere: "Talvez a viga suporte até 10kg?". O sistema testa. Se errar, a IA ajusta. É como ter um estagiário muito esperto que chuta as regras, e um supervisor rigoroso que corrige os erros.

5. O Resultado: Ferramenta "Dualis"

Os autores criaram uma ferramenta chamada Dualis e testaram com bibliotecas de código reais e grandes (como as usadas pelo Facebook e Google).

O que eles descobriram: O sistema conseguiu verificar programas que ferramentas antigas de verificação automática não conseguiam resolver.
A vantagem: Eles conseguiram lidar com bibliotecas gigantes sem precisar ler cada linha de código delas, apenas garantindo que elas passassem nos testes específicos para o contexto do programa.

Resumo em uma frase

Em vez de tentar provar que a fábrica inteira é perfeita (o que é impossível), o sistema cria regras específicas para como você usa a fábrica, testa essas regras exaustivamente e, se passarem, permite que você construa sua casa com confiança. É uma abordagem pragmática que troca a perfeição teórica pela segurança prática e escalável.

Resumo Técnico: Verificação Modulo Contratos de Bibliotecas Testadas

1. O Problema

O artigo aborda um dos maiores gargalos na verificação formal de software em escala: a dificuldade de verificar automaticamente programas clientes que utilizam bibliotecas complexas e grandes.

O Dilema Atual: A verificação completa e automatizada de grandes bases de código é atualmente inviável. Métodos tradicionais exigem anotações humanas (contratos e invariantes) tanto para o cliente quanto para a biblioteca. Sintetizar invariantes indutivos e contratos para bibliotecas complexas é um problema de busca difícil que as técnicas atuais não conseguem escalar.
A Proposta: Os autores propõem um novo paradigma chamado Verificação Modulo Contratos de Bibliotecas Testadas (VMTLC). A ideia central é relaxar a garantia de verificação formal para a biblioteca, substituindo-a por testes extensivos.
Definição do Problema: Dado um programa cliente $C$ $C$ que usa uma biblioteca $L$ $L$ , o objetivo é sintetizar automaticamente:
1. Um conjunto de contratos formais $\Pi$ para os métodos da biblioteca.
2. Invariantes indutivos para o código do cliente.
3. Condições de Sucesso: (a) O cliente deve ser provado correto assumindo os contratos $\Pi$ ; e (b) Os contratos $\Pi$ devem passar em um gerador de testes determinístico que tenta encontrar violações na implementação real da biblioteca.

2. Metodologia e Framework

O trabalho apresenta um framework de aprendizado guiado por contraexemplos (CEG) que sintetiza simultaneamente contratos para a biblioteca e anotações para o cliente.

Abordagem Iterativa (CEG):
1. Síntese: Um solucionador de CHC (Constrained Horn Clauses) generalizante tenta encontrar contratos e invariantes que satisfaçam as condições de verificação do cliente.
2. Teste: Um gerador de testes (implementado com AFL++) verifica se os contratos sintetizados são violados pela implementação real da biblioteca.
3. Refinamento: Se o teste falhar, os casos de teste que violaram o contrato são tratados como exemplos positivos e adicionados ao conjunto de dados para o solucionador.
4. Repetição: O solucionador re-sintetiza os contratos, garantindo que eles cubram os novos exemplos positivos, até que o cliente seja provado e os contratos passem nos testes.
Contratos Contextuais vs. Modulares:
- Contratos Modulares: Devem valer para qualquer estado e entrada possível da biblioteca. São difíceis de sintetizar.
- Contratos Contextuais (Novidade): São contratos que valem apenas no contexto específico em que o cliente chama a biblioteca. Como o cliente impõe pré-condições implícitas (ex: "só insere números positivos"), os contratos podem ser mais fortes e simples (ex: "retorna falso para números negativos"). O framework testa esses contratos executando o programa completo (cliente + biblioteca), não apenas a biblioteca isoladamente.
Algoritmos de Aprendizado (ICE):
O núcleo do solucionador utiliza ICE-learning (Implication Counterexample), que lida com exemplos positivos, negativos e de implicação. O artigo explora três realizadores para o solucionador CHC generalizante:
1. HornICE: Um algoritmo baseado em árvores de decisão que busca expressões lógicas simples.
2. LLMs (Large Language Models): Uso de modelos de linguagem (como Gemini) para propor contratos e invariantes, atuando como aprendizes ICE.
3. Híbrido (HornICE + LLM): O LLM gera predicados atômicos (base) e o HornICE constrói as árvores de decisão combinando-os, garantindo generalização e correção lógica.
Ferramenta: O framework foi implementado em uma ferramenta chamada Dualis.

3. Contribuições Principais

Definição Formal do Problema VMTLC: Formalização da verificação de clientes onde a biblioteca é apenas testada contra contratos sintetizados, não provada formalmente.
Contratos Contextuais: Introdução e formalização de contratos que são válidos apenas no contexto de execução do cliente, permitindo especificações mais simples e fáceis de inferir do que contratos modulares clássicos.
Framework de Síntese Unificada: Um algoritmo que sintetiza simultaneamente invariantes do cliente e contratos da biblioteca, utilizando um ciclo de aprendizado guiado por testes e verificação.
Integração de LLMs: Demonstração de como LLMs podem ser integrados a frameworks de verificação formal como aprendizes ICE, utilizando contraexemplos para refinar suas sugestões.
Implementação e Avaliação: A ferramenta Dualis e uma suite de benchmarks robusta.

4. Resultados da Avaliação

Os autores avaliaram o framework em 43 benchmarks C++ derivados de bibliotecas de código aberto populares (Folly, Abseil, Android) e do SV-COMP.

Eficácia:
- O framework foi capaz de verificar clientes que ferramentas de estado da arte (como SeaHorn) falharam em verificar completamente.
- LLMs: O aprendizado baseado em LLM puro foi o mais eficaz, resolvendo 38/43 benchmarks com contratos modulares e 41/43 com contratos contextuais.
- HornICE: Resolveu menos casos (19/43 modulares), frequentemente falhando devido à falta de predicados expressivos em seu template fixo.
- Contratos Contextuais: Foram consistentemente mais fáceis de sintetizar e mais rápidos de encontrar do que os modulares, resolvendo mais benchmarks com contratos menores e menos complexos.
Validade dos Contratos:
- Todos os contratos sintetizados foram verificados manualmente e logicamente (usando solvers de restrições) para garantir que eram implicações válidas dos contratos de referência.
- O teste com AFL++ mostrou alta cobertura de código (média de 50% de cobertura de bitmap) e estabilidade de 100%, indicando que os contratos sintetizados são robustos contra violações comuns.
Estudo de Mutantes (Segurança):
- O estudo analisou se o framework poderia "provar" programas incorretos.
- Contratos Modulares: Rejeitaram todos os mutantes incorretos criados (que continham caminhos de execução raros).
- Contratos Contextuais: Verificaram incorretamente 11/30 mutantes. Isso ocorre porque os contratos contextuais são testados apenas no contexto do cliente; se o caminho de erro é raro e não é atingido pelos testes do cliente, o contrato espúrio passa. Isso destaca um trade-off: contratos contextuais são mais fáceis de sintetizar, mas oferecem garantias ligeiramente menores contra bugs raros não cobertos pelos testes.

5. Significado e Conclusão

O artigo representa um avanço significativo na direção da verificação automatizada escalável para software real.

Mudança de Paradigma: Propõe que, para escalar a verificação a grandes bibliotecas, é aceitável substituir a prova formal da biblioteca por testes rigorosos, desde que o cliente seja provado formalmente sob os contratos sintetizados.
Viabilidade Prática: Demonstra que a combinação de solvers de CHC, testes de fuzzing e LLMs pode superar as limitações atuais da verificação automática, permitindo a análise de programas que antes eram intratáveis.
Futuro: O trabalho sugere que os contratos contextuais têm valor mesmo em cenários semi-automáticos (onde engenheiros escrevem anotações), e abre caminho para a síntese de observadores de estado e a aplicação em lógicas mais complexas (como manipulação de heaps compartilhados).

Em resumo, o VMTLC oferece um caminho prático para garantir a correção de sistemas complexos, equilibrando a rigidez da prova formal com a eficiência da síntese automatizada e testes.