Skip to main content
PPGEE/UFAM

Trabalho em anais de eventoOpen Access

ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference

GADELHA, M. Y. R.; SOUSA, F. R. M.; CORDEIRO, L. C.; NICOLE, D

2019 • International Conference on Tools and Algorithms for the Construction and Analysis of Systems • 55 citações

Resumo

Resumo

ESBMC v6.0 employs a k -induction algorithm to both falsify and prove safety properties in C programs. We have developed a new interval-invariant generator that pre-processes the program, inferring invariants based on intervals and introducing them in the program as assumptions. Our experiments show that ESBMC v6.0 using k -induction can prove up to 7% more programs when the invariant generation is enabled.

palavras-chave

Palavras-chave

ESBMCk-inductioninvariant inferenceC program verificationsafety verificationfalsificationprogram verification tools

Status

Published

links

DOI

10.1007/978-3-030-17502-3_15

Link Externo

https://doi.org/10.1007/978-3-030-17502-3_15

Repositório

https://research.manchester.ac.uk/en/publications/3cb76910-17cb-4656-b277-d36da785c565

Abrir publicação

Trabalho em anais de evento

Leveraging Template Matching for Efficient Android Screenshot Visual InspectionMYRRIA, ABDA; CASTRO, ALICE; MUNIZ, CAIQUE; BARBOSA, HERYCK; SILVA, ANDRÉ; CORDOVIL, LUIZ; PORTY, ROGER; SOUTO, THIAGO2026 • 2026 IEEE International Conference on Consumer Electronics (ICCE)1citações
Comparative Evaluation of DNNs and Template Matching for GUI Validation on Android DevicesMYRRIA, ABDA; CASTRO, ALICE; MUNIZ, CAIQUE; BARBOSA, HERYCK; SILVA, ANDRÉ; CORDOVIL-JR, LUIZ; PORTY, ROGER; SOUTO, THIAGO2026 • 2026 IEEE International Conference on Consumer Electronics (ICCE)
LLM-based text-to-JQL Generation: an automated test using execution and structural indicatorsLIMA, RAYFRAN ROCHA; DE BRITO, IRINEU EVANGELISTA CRUZ; NASCIMENTO, JARDEL DA CUNHA; CORDOVIL-JR, LUIZ2026 • 2026 IEEE International Conference on Consumer Electronics (ICCE)
Bearing fault prognosis based on evolving granular modelsMARTINIANO, ALEXANDRE; VITÓRIO, ANDEVALDO; AYRES, FLORINDO; OTANI, MARIO; MEDEIROS, JOSÉ; NUNES, RIVELINO; SILVA, RENAN; VARELA, JERRY; MOURA, DAVIDSON; SANTOS, KENNY; COSTA, JEFERSON; MENDONÇA, RAFAEL; BESSA, IURY2026 • XX Simpósio Brasileiro de Automação Inteligente (SBAI 2025) e XII Simpósio Brasileiro de Sistemas Elétricos (SBSE 2025)

Ver todas as publicações