This paper proposes a counterexample-guided narrowing approach, which mutually refines analyses and testing if (possibly spurious) counterexamples are found. A prototype tool CANAT for checking roundoff errors between floating point and fixed point numbers is reported with preliminary experiments.

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.