Reasoning about loops is knowingly hard as Hoare triple-like verification requires inductive loop invariants to prove properties over loops. A loop invariant basically abstracts the behaviour of a loop with logic, that is a loop invariant is a formula that holds before the loop, after the loop, as well as after each iteration of the loop. Furthermore a loop invariant must be strong enough to derive a safety property that we want to prove for a given program. Of course there exist programs for which loop invariants are not in the first-order fragment but require some higher-order logic to be expressed. However, for many programs loop invariants are actually expressible as first-order logic formulae. Thus, loop invariant generation is a major research area when it comes to automated program reasoning.

Most such tools however are inherently limited by using SMT-solvers to discharge verification conditions. Their limitations when it comes to quantified reasoning are well-known; they usually work well with universal quantification and theories, but are limited in existential quantification and hence also alternating quantification, i.e. a combination of universal and existential quantifiers in the loop invariants. As a consequence most automated invariant generation tools are also limited to universally quantified loop invariants and can rarely handle potentially necessary existential or alternating quantification. 

Since our verification framework RAPID is based on full first-order theorem proving, that is also handling existential quantification and quantifier alternations, we wanted to leverage our tool for invariant generation as well. To this end, we extended our framework with the symbol elimination approach that allows to synthesize arbitrarily quantified clauses that in conjunction can form a quantified loop invariant with the help of first-order theorem prover Vampire; these invariants could further be supplied to other verification tools, thus complementing invariant generation efforts in the area.

To do so, we use a special mode of Vampire to derive logical consequences of the semantics produced by RAPID. Some of these consequences may be loop invariants. The symbol elimination approach defines some set of program symbols undesirable, and only reports consequences that have eliminated such symbols from their predecessors. In RAPID, we adjust symbol elimination for deriving invariants in trace logic using Vampire. These invariants may contain quantifier alternations, and some conjunction of them may well be enough to help other verification tools show some property. 

The symbol elimination method: In general loop invariants should not contain symbols other than from the input language, that is given that our encoding requires trace logic we want to rid ourselves from trace logic specific symbols. In our case that means we want to eliminate symbols containing timepoints and only find consequences that do not contain such symbols. However, we still want to generate invariants containing otherwise-eliminated variables at specific locations, that is we still want to find consequences of timepoint reasoning, but express them without such symbols in it. To remove such constructs, we apply symbol elimination: any symbol representing a variable v used on the left-hand side of an assignment is eliminated. For each eliminated variable v we define a set of interesting timepoints l1, l2 … and declare constants v_init = v(l1) and v_final = v(l2) for appropriate locations l1,l2. Specifically, we want to derive information about program variables at the beginning as well as the end of program executions, so we will mostly choose these timepoints to be before a loop and after a loop. These new symbols now do not need to be eliminated.

This allows other tools to make use of trace logic reasoning to guide the search for quantified invariants. Moreover, the given set of consequences can easily be verified to prove a program property by trying to derive a safety property merely from the generated consequences. Proofs of such sort are in general very short and fast, given that the set of generated consequences contains the necessary loop invariant. 

To use RAPID in invariant generation mode, we added a new flag -invariantGeneration on to the framework allowing to derive logical consequences with the symbol elimination approach.