Trabalho em anais de eventoOpen Access
LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling
PIRZADA, M. A. A.; BHAYAT, A.; CORDEIRO, L. C.; REGER, G
Resumo
Resumo
We investigate a modification of the classical Bounded Model Checking (BMC) procedure that does not handle loops through unrolling but via modifications to the control flow graph (CFG). A portion of the CFG representing a loop is replaced by a node asserting invariants of the loop. We generate these invariants using Large Language Models (LLMs) and use a first-order theorem prover to ensure the correctness of the generated statements. We thus transform programs to loop-free variants in a sound manner. Our experimental results show that the resulting tool, ESBMC ibmc, is competitive with state-of-the-art formal verifiers for programs with unbounded loops, significantly improving the number of programs verified by the industrial-strength software verifier ESBMC and verifying programs that state-of-the-art software verifiers such as SeaHorn and VeriAbs could not.
palavras-chave
Palavras-chave
bounded model checkingloop invariantslarge language modelsloop unrollingfirst-order theorem provingsoftware verificationformal verification
Status
Published
links
Links e arquivos
Trabalho em anais de evento