Sign Analysis as Symbolic Execution

Sign analysis performs Over-Approximation in symbolic execution

For variables $V = \{x,y\}$ the symbolic state is:

   x=x_k \land y=y_k \land (P(x) \land P(y))

where $P(x)$ is one of the formulas $x<0$, $x=0$, $x>0$, or 'true' (and similarly for $P(y)$)

Initially, we approximate initial state (if unknown, then $P(x),P(y)$ are true)

When we compute strongest postcondition, then we approximate it to obtain again formula in the previous form

Use a work-list algorithm to propagate symbolic state in the presence of loops

We go through loop several times until values stabilize