Sign Analysis as Symbolic Execution

Sign analysis performs Over-Approximation in symbolic execution

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

$\begin{equation*} x=x_k \land y=y_k \land (P(x) \land P(y)) \end{equation*}$

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