Completeness of Pointer Program Verification by Separation Logic

This paper proposes a framework for statically analyzing overflow and roundoff errors of C programs. First, a new range representation, ``extended affine interval'', is proposed to estimate overflow and roundoff errors. Second, the overflow and roundoff error analysis problem is encoded as a weighted model checking problem. To avoid widening, currently we focus on programs with bounded loops, which typically appear in encoder/decoder reference algorithms. Last, we implement the proposed framework as a static analysis tool CANA. Experimental results on small programs show that the extended affine interval is much more precise than classical interval.