Code2Inv is a general end-to-end deep learning framework which learns a valid loop invariant for any given verification task.
Automated program verification is an extremely difficult task, especially for practical programs. A major challenge lies in effective proof search. Finding loop invariants is arguably the most crucial part of this proof search.
So what is a loop invariant? A loop invariant, simply put, is a condition that is true before and after each iteration of a loop. Proofs for instances containing loops can be found if the correct loop invariant is inferred for each loop. However, inferring these loop invariants is a complicated process which can prove to be challenging even for seemingly simple programs.
Code2Inv is a framework which infers loop invariants for a given task. It is based on the Counter-Example Guided Inductive Synthesis (CEGIS) paradigm, where a generator proposes a candidate solution and a checker determines the correctness of this candidate solution. Code2Inv works in a multi-step decision making process similar to how human experts construct loop invariants. Code2Inv leverages reinforcement learning to learn the features of the task and infer the invariant without the need of any supervision.
Code2Inv is a general framework. As long as the inputs provided match the general requirements, it is possible to use Code2Inv. The inputs are such that instances in several languages can be easily reduced to the input requirements. We demonstrate this with C programs and CHC constraints, but this could be extended to other languages as well.