With the forward (strongest postcondition) verifier, the polarity of all memory domains is always negative (i.e. memory domains only accumulate values that are not equivalent). By committing to only supporting negative-polarity domains, we can significantly simplify their implementation.
With the forward (strongest postcondition) verifier, the polarity of all memory domains is always negative (i.e. memory domains only accumulate values that are not equivalent). By committing to only supporting negative-polarity domains, we can significantly simplify their implementation.