Automatic generation of loop invariants

CppInv works in two stages. Firstly, it parses a source code written in a subset of C++ and abstracts all execution paths of the program building a control flow graph associated to a transition system. Paths are expressed as arbitrary propositional formulas over linear integer arithmetic including high level operators like integer division and modulo. That makes easy the initial modeling. Later, formulas are normalized and only paths between a set of locations that cover every cycle of the control flow graph are regarded. Secondly, CppInv generates linear invariants at the selected locations setting out a constraint solving problem. We present a method to discover all linear invariant of the considered form. As a result, our tool can find linear invariants efficiently for a large set of interesting programs. Moreover, CppInv is also able to generate some non-linear invariants automatically. For instance, it is possible to prove the total correctness of a program that multiplies two integers from the invariants returned by the tool