Skip to main content
PPGEE/UFAM

Trabalho em anais de eventoOpen Access

DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs

ROCHA, W.; Rocha, H.; ISMAIL, H. I.; CORDEIRO, L. C.; FISCHER, BERND

2017 • 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems • 36 citações

Resumo

Resumo

DepthK is a software verification tool that employs a proof by induction algorithm that combines k-induction with invariant inference. In order to efficiently and effectively verify and falsify safety properties in C programs, DepthK infers program invariants using polyhedral constraints. Experimental results show that our approach can handle a wide variety of safety properties in several intricate verification tasks.

palavras-chave

Palavras-chave

k-inductioninvariant inferenceprogram verificationC programssafety propertiespolyhedral constraintsmathematical inductionfalsificationsoftware verification tools

Status

Published

links

DOI

10.1007/978-3-662-54580-5_23

Link Externo

https://doi.org/10.1007/978-3-662-54580-5_23

Repositório

https://research.manchester.ac.uk/en/publications/9362de30-adb6-4799-9220-4007ab3fe610

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