Code-2Inv

The 'Code-2Inv' dataset is a benchmark that contains C programs along with their formal preconditions and postconditions, 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 Solvers2025FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving2024 · 2 citesCLN2INV: Learning Loop Invariants with Continuous Logic Networks2019