Code-2Inv

The Code2Inv benchmark contains C programs along with their formal preconditions and postconditions, and it is used to evaluate the effectiveness of methods for synthesizing loop invariants.

Papers using Code-2Inv (3)

Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers2025CLN2INV: Learning Loop Invariants with Continuous Logic Networks2019FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving2024