Interval counterexamples for loop invariant learning

我们组的工作

Counterexample Generalization

Let $\psi$ be the formula and $\sigma (x)$ assigns ${\mu }_x$ to variable x, which is a violating model of $\psi$

Variable Elimination

The formula $\psi \wedge {\bigwedge }_{x}x={\mu }_x$ is hence unsat.

By making $\psi$ hard and ${\bigwedge }_{x}x={\mu }_x$ soft constraints, the unsat core signifies a subset of variables $x_c\subseteq x$

Boundary Constraints

Let D = d1, d2, … dm be a fixed set of distance with d0 =0, then the following formula

$$\psi \wedge \underset{x}{\bigwedge }\bigwedge \{x\ge {\mu }_x-d_i,x\le {\mu }_x+d_j\mid 0\ge i,j\le m\}$$

is unsat. The unsat core gives an interval to each variable.

The soft constraints here overlap, thus the obtained interval might not be the maximal ones

Interval Digging

and update the formula to:

The unsat core {$I_1,I_2,...I_m$} is joint and ${\wedge }_{i=1}^m{I}_i$ represent (possible several disjoint) interval for a variable,