SMART ESBMC/JBMC — Verificação Formal

Ambiente …

Nova verificação

Pasta do projeto/benchmark

estratégia (?) incremental/k-induction ignoram o unwind fixo e valem só para C — em Java/Kotlin o JBMC usa bounded

verificação de overflow (?)

checar overflow unsigned (size_t/unsigned)

unwind (?) mín 1 · típico 5–20

timeout (s) (?) mín 1 · típico 30–120

jobs (?) mín 1

solver (?)

Opções de projeto (avançado)

include paths (-I) (?) um diretório por linha

unidade multi-arquivo (link) (?) um arquivo por linha (relativo à pasta)

função-entrada (--function) (?) vazio = usa o main()

Resultados

Distribuição CWE

Alvos (clique para ver o contraexemplo)

Alvo	Tipo	Status	Bug	CWE	CERT

Reparo guiado por contraexemplo dry-run

dry-run

só os que faltam

Clique num alvo para ver a trilha e o código corrigido.

Alvo	Bug	Resultado	Iterações

Repara os alvos com BUG desta run (LLM propõe → o verificador valida → realimenta o contraexemplo até provar a correção). Em dry-run demonstra o loop sem usar a API.

Histórico (clique para abrir o relatório)