LPI: Software Verification with Local Policy Iteration

LPI is a module for invariant generation embedded inside the CPAchecker framework. It uses a local policy iteration approach, which allows it to obtain precise numerical invariants. The approach performs computations in the template constraints domain using maximization modulo SMT, and terminates with a potentially over-approximating inductive invariant. Local policy iteration is a sound, but incomplete technique which obtains numerical, conjunctive inductive invariants for the analyzed programs. It can prove programs to be safe by finding a separating inductive invariant, but can not find counterexamples to safety. We supply the generated inductive invariant to the k-induction procedure, which terminates with either a counterexample or a proof of safety.