JAIST Repository
https://dspace.jaist.ac.jp/

Title

Combining Testing and Static Analysis to Overflow
and Roundoff Error Detection

Author(s)Do, Ngoc Thi Bich; Ogawa, Mizuhito

Citation

Research report (School of Information Science,
Japan Advanced Institute of Science andTechnology), IS‑RR‑2010‑004: 1‑27

Issue Date

2010‑06‑21

TypeTechnical Report

Text version

publisher

URL

http://hdl.handle.net/10119/9018

RightsDescription

リサーチレポート（北陸先端科学技術大学院大学情報科学研究科）

Japan Advanced Institute of Science and Technology

Combining Testing and Static Analysis to Overflow andRoundoff Error Detection
Do Thi Bich Ngoc  Mizuhito Ogawa.

Abstract This paper proposes a technique for automatic detection of overflow and roundoff errors, causedby the floating-point number to fixed-point number conversion. First, a new range representation, “extended
affine interval”, is proposed to overapproximate overflow and roundoff errors. Second, the overflow and roundoff error analysis problem is encoded as a weighted
model checking, which is implemented as a static analyzer CANA. Last, we propose a new testing refinement loop, called “counterexample-guided narrowing”,
by combining the static analysis and testing. They arecomposed and implemented in a prototype tool, CANAT,
in which analysis results are used not only for possible
roundoff error detection, but also for finding dominanterror factors in input parameters. To avoid widening,
currently we focus on programs with bounded loops
and arrays with fixed length, which typically appear
in encoder/decoder reference algorithms. Experimental
results on small programs show that the extended affineinterval is much more precise than classical interval, andthe counterexample-guided narrowing approach outperforms the random testing technique.

Do Thi Bich Ngoc
School of Information Science - Japan Advanced Institute of Science and Technology
Tel.: +84-0761-51-1247
Fax: +84-0761-51-1149
E-mail: dongoc@jaist.ac.jp
Mizuhito Ogawa
School of Information Science - Japan Advanced Institute of Science and Technology
Tel.: +84-0761-51-1247
Fax: +84-0761-51-1149
E-mail: mizuhito@jaist.ac.jp

Keywords Software verification  Static analysis Testing  Roundoff error  Overflow error  Affineinterval  Classical interval
1 Introduction
In the computers, a real number has a finite representation, i.e., either a floating-point number, or a fixedpoint number, which may introduce overflow and roundoff errors (ORE). OREs cause tricky behavior; for instane, consider

p333.75  a2 qb6 a2 p11a2 b2  121b4  2q 5.5b8 pa{p2bqq
for a  77617, b  33096. This is known as Rump’s
example [31] and IEEE 754 standard floating operations [22] return the results
Single precision 1.172604
Double precision 1.1726039400531786
Fourfold precision 1.17260394005317863185883490452
011838which seem that the single precision is enough. However, if we symbolically compute with rational number
representations, it will result 54767{66192 (approx.
0.8273960599).
Overflow and roundoff errors problem
A famous example that caused a serious disaster byroundoff errors is “The Patriot Missile Failure” 1 .
On February 25, 1991, during the Gulf War, an
American Patriot Missile battery in Dharan, Saudi Arabia, failed to track and intercept an incoming Iraqi Scudmissile. The Scud struck an American Army barracks,
killing 28 soldiers and injuring around 100 other people.
1

http://www.ima.umn.edu/ arnold/disasters/patriot.html

2

The reason is roundoff error cause by representing
the real number p1{10q by the fixed-point number.
1{10  1{24

1{25

1{28

1{29

1{212

1{213

...

which corresponds to the binary expansion of 1/10
0.0001100110011001100110011001100...
The 24 bit register in the Patriot stored instead
0.00011001100110011001100
introducing an error of
0.0000000000000000000000011001100...
(in binary), which is about 0.000000095 in decimal.
Multiplying by the number of tenths of a second in 100
hours gives 0.000000095  100  60  60  10  0.34.
A Scud travels at about 1,676 meters per second, andthus travels more than an half kilometer in this time.
Another famous example of overflow errors is “The
Explosion of the Ariane 5” 2 .
The ORE problems have been one of the central
issues in the numerical analysis [17,13]. There are threekinds of OREs, caused by:– real numbers to floating-point numbers conversion,– real numbers to fixed-point numbers conversion, and– floating-point numbers to fixed-point numbers conversion.
The first category is most extensively investigated.
There are lots of works on mathematical reasoning toestimate OREs, and there is a well-known methodology
for precise addition and subtraction, which concern theeffect of REs [27]. For nonlinear operations, such as
multiplication and division, recently verified numericalcomputation is evolving.
We focus on ORE problems from a different view
point, static detection. There are several examples of
ORE analyses on the real numbers to floating-point
numbers conversion [20,21,33,38], including tool implementations [20, 38, 34].
We focus on ORE anslyses again from a different
view point, the floating-point numbers to fixed-point
numbers conversion. Our motivation comes from practical demands in industry. They had troubles on converting a DSP reference algorithm into a hard-wired one,along with the floating-point numbers to fixed-point
numbers conversion. Apart from difficulties in hardware
encoding [3, 5, 25, 26,37,51,52], OREs may cause visible
decoding errors.
2

http://www.ima.umn.edu/ arnold/disasters/ariane.html

For the floating-point numbers to fixed-point numbers conversion, an ORE analysis was proposed in [9–11] with the same motivation. They used a sophisticated representation, Classical interval (CI) [2, 40] andAffine interval (AI) [54, 55]. CI is simple but imprecise,because it does not handle correlations between variables. AI introduces symbolic manipulations on noise
symbols, to handle correlations between variables. AI
arithmetic supplies higher precision, especially in linear operations (e.g., addition, subtraction). However,AI introduces a fresh noise symbol at each nonlinear
arithmetic operation, which may lead potential inefficiency. The problem raises a natural question: Can wecreate a new interval that is simpler yet precise as AI?
We also observe the fact that OREs of the floatingpoint numbers to fixed-point numbers conversion can betested, since we can compute both floating-point numbers and fixed-point numbers.
Target programs
Motivated by practical demands, our target programs are reference C algorithms for DSP encoders and
DSP decoders.
Our observation on DSP encoders/decoders is thatthey contain unbounded loops, pointers manipulation,
dynamic arrays manipulation only in the outermost interface of large input data (e.g., sound, video). The input data are divided into small pieces and processedby the core algorithm (e.g., Invert Direct Cosine Transform algorithm), which (mainly) consists of loops witha bounded number of iterations and arrays with a fixed
size [47]. For instance, in the Mpeg decoder, typical arrays have size 88, typical loops are 88, and the outermost loop iterates depending on the resolution (Fig. 1)

8×8
loop

8×8
loop

…

8×8
loop

Outermost loop depending on resolution
Fig. 1 Typical loops in Mpeg decoder

Based on this observation, we restrict targets toa subclass of C programs with bounded loops, fixed
size arrays, no pointer manipulations, and no procedure
calls.
Then, we set the ORE problems as follows:
Given a program, initial ranges of input parameters,
and the fixed-point format,

Not safe!
-0.26

1.
2.
3.
4.
5.

/* CANAT
CANAT ALL sign 11 4
maintest x range -1 3
maintest y range -10 10_test global rst 0.26*/
typedef float Real;
Real rst;
Real maintest(Real x, Real y){if (x>0){rst=x*x;}else rst = 3*x;
rst = rst - y;return rst;
}

0

0.26

rstr

3

No
counterexamples!

-0.26

0

0.26 rstr

a. roundoff error of rst found by testing r0.20, 0.21s
Not safe!

-0.26

0

0.26

rstr

Fig. 2 An example of a C program
b. roundoff error of rst found by analysis

 r0.28, 0.28s
No

1. Whether the largest RE of a result lies within given
threshold?
2. Whether overflow error may occur?
3. If they occur, where?
We say that the program is “safe” if for all inputs,
REs of the result lie in rθ, θs.
Example 1 Fig. 2 shows a C program with annotations
that:– initial ranges of x, y: x P r1, 3s, y P r10, 10s,
– fixed-point format p11 : 4q, and– RE threshold is θ  0.26
Note that base b  2.
The questions are:
1. Does RE of rst lie within r0.26, 0.26s?
2. May overflow error occur? Where?
The OREs will be propagated through computations of the program. Further, the computations themselves cause OREs because the arithmetic needs to roundthe result to fit the number format. Besides, OREs arealso affected by types of statements (e.g., branch, loop,
assignment).
Testing vs static analysis
We may face a situation that an ORE analysis reports that the roundoff error of the result exceeds theroundoff error threshold, but a test cannot find any
counterexamples.
Example 2 Assume that for the program in Fig. 2, theinitial ranges of x, y are r1, 3s, r10, 10s, respectively.
The conversion from the floating-point type to fixedpoint type such that the width of integer part is 11 andthe width of fraction part is 4. It is safe if no overflow
errors occur and no roundoff errors of rst go beyondr0.26, 0.26s.

Fig. 3 Results of analyzing and testing C programin Fig. 2
counterexamples!

By random 100 test cases, all roundoff errors lie in
rstr-0.26 r0.20, 0.21
0 s  r0.26,0.26
the range
0.26s, whichmeans
no counterexamples are found (Fig. 3 a).
The ORE analysis (in Section 4) reports that theroundoff error of rst lies in r0.28, 0.28s, which exceeds
the roundoff error threshold r0.26, 0.26s (Fig. 3 b).
Then, both testing and analysis cannot clarify whether
the program in Fig. 2 is safe.
The challenge is how to bridge the gap between testing and static analysis?
Main results and paper structureThis paper proposes a technique for automatic detection of overflow and roundoff errors, caused by thefloating-point number to fixed-point number conversion. First, inspired by the range representation to under approximate OREs [21], a new range representation, extended affine interval (EAI) is proposed to overapproximate OREs. EAI does not increase the numberof noise symbols.
Second, the overflow and roundoff error analysis problem is encoded as a weighted model checking, which is
implemented as a static analyzer CANA. A weight domain is designed based on the EAI arithmetic.
Last, we propose a new testing refinement loop,
called “counterexample-guided narrowing”, by combining the static analysis and testing. This refinement of
testing is performed by detected OREs by CANA, inwhich EAI shows dominant error factors among input
parameters. They are composed as a prototype tool,
CANAT.
To avoid widening, currently we focus on programswith bounded loops and arrays with fixed length, which
typically appear in encoder/decoder reference algorithms.
Experimental results on small programs show thatthe extended affine interval is much more precise than

4classical interval, and the counterexample-guided narrowing approach clearly outperforms the random testing technique.
The rest of this paper is organized as follows. Section 2 formally presents ORE problems. In Section 3,
we introduce various interval arithemtic. We also propose a new range representation, EAI, adding to traditional CI and AI. The ORE analysis based on weighted
model checking is introduced in Section 4. We also describe the implementation of the proposed framework ina tool, CANA. Section 5 proposes the counterexampleguided narrowing approach to detect REs and its implementation, CANAT. Section 6 overviews related works.
Finally, Section 7 concludes the paper and indicates future works. The content of Section 3 to 4 and that of
Section 5 were preliminary reported in [44] and [45],respectively.

Example 3 The decimal number x  8.75, represented as p1q0  0.875  101 , has s  0, m  0.875, e 
1. Its equivalent binary format is x  p1q0 p0.100011q
2100 with s  1, m  0.100011, e  100. The corresponding normal floating-point number is x p1q0 p1.00011q 210 with s  1, m  1.00011, e  10.
The floating-point format pb, p, emaxq determines a
set of representable floating-point numbers, in which:– b is base (e.g. 2 or 10)– p is number of digits in the significand– emax is the maximum value of exponent e (the minimum value of e is emin  1  emaxq.
We basically follow the IEEE7542008 standard [22],shown in Table 1. Thus, a normal floating-point number
closest to zero is bemin and a number farest from zerois pb  b1p q  bemax . For instance, in the binary 64
floating-point format,– The number closest to zero is

2 Representation of Real Numbers and theORE Problem

21022  2.225073858507202010308

We first present overflow and roundoff error (ORE)
problem when represent real numbers in computers suchas floating-point numbers (Subsection 2.1) and fixedpoint numbers (Subsection 2.2). In Subsection 2.3, we
introduce ORE arithmetics, which decomposes a number into a pair of floating-point (or fixed-point) and aroundoff error evaluation.

– The number farest from zero ispp1p1{2q53 q21024 q  1.797693134862315710308
2.1.2 OREs of Floating-point Numbers
Since floating-point numbers have the finite precision,roundoff error may occur due to the finite fraction part,and overflow error may occur due to the finite integer
part.

2.1 Floating-point Numbers and ORE problem
2.1.1 Floating-point Numbers
Floating-point numbers are often used to represent real
numbers in numerical computation. In a floating-point
number, the position of the radix point is dynamic.
Definition 1 A floating-point number x has a representation in base b, with sign s, significand m, andexponent e, such thatx  p1qs  m  be(1)

where s is 0 or 1, m  d0 .d1 ...dp1 with 0 ¤ di b,
and e is an integer. The set of floating-point numbers is denoted by Rf l
Remark 1 In order to optimize the quantity of representable numbers, floating-point numbers are typicallyin normalized form, which puts the radix point after
the first non-zero digit (e.i., d0  0).

Roundoff error (RE) If the significand m of x is represented by more than p bits, x will be truncated (orchopped) in some way. The IEEE7542008 standard defines four rounding algorithms [22].
– Round to Nearest: This is the default mode. In thismode results are rounded to the nearest representablevalue. If the result is midway between two representable values, the even representable is chosen.
Even here means the lowest-order bit is zero.
– Round toward 0 : All results are rounded to the largest
representable value whose magnitude is less thanthat of the result. In other words, if the result is negative it is rounded up; if it is positive, it is roundeddown.
– Round toward 8: All results are rounded to thesmallest representable value, which is greater than
the result.
– Round toward 8: All results are rounded to thelargest representable value, which is less than the
result.

5parameterbpemax

binary322
24+127

binary64
2
53
+1023

binary1282113+16383decimal32
107+96

decimal64
10
16
+384

decimal128
10
34
+6144

Table 1 The formats of floating-point numbers

Definition 2 Let x be a real number and let xf l beits floating-point number representation. The roundoff
error (RE) is ref l pxq  x  xf l .
Example 4 In the IEEE 754 decimal32 format (b 10, p  7, emax  96),
Floating-point representation For x  10{3, its floatingpoint number representation is xf l  p1q0 3.3333333
100 and the RE is
ref l pxq  0.0000000333333333333333333333333....
Floating-point additione = 5 m = 1.234567(123456.7)+ e = 2 m = 1.017654(101.7654)
e = 5 m = 1.234567+ e = 5 m = 0.001017654 (after shifting)e = 5 m = 1.235584654
This is the exact sum of the operands. It will be
rounded to seven digits and then normalized (if necessary). The final result is e  5; m  1.235585, and thelow 3 digits of the second operand (654) are lost. The
RE of the addition is p1q0  0.000000654105  0.0654.
Floating-point multiplicatione = 3 m = 4.734612
e = 5 m = 5.417242
e = 8 m = 25.648538980104 (true product)e = 8 m = 25.64854 (after rounding)e = 9 m = 2.564854 (after normalization)
In this case, the lost information of the significand
m after normalization are (-0.0000001019896). The RE
of the multiplication isp1q  0.0000001019896  10  101.9896
1

9

Based on rounding mode, the value of RE may differ.
Lemma 1 For real number x and its normal floatingpoint representation xf l , the RE ref l pxq satisfy:|ref l pxq{x| ¤ Emach where– Emach  b1p for the rounding toward zero, and– Emach  b1p {2 for the rounding to nearest.

Overflow error (OE) If the exponents e of x is greaterthan emax, it is an overflow error (OE). More precisely, for a real number x and its floating-point format
pb, p, emaxq, if x ¡ pb  b1p q  bemax , an OE occurs.
Example 5 In the IEEE 754 decimal32 format (b 10, p  7, emax  96),e = 48 m = 4.734612
 e = 48 m = 5.417242
e = 96 m = 25.648538980104 (true product)e = 96 m = 25.64854 (after rounding)e = 97 m = 2.564854 (after normalization)
Since e ¡ emax, an OE occurs.
2.2 Fixed-point Numbers and ORE Problem
2.2.1 Fixed-point Numbers
Fixed-point numbers are a simple and an easy way toexpress real numbers, using a fixed number of digits.
Due to the hardware simplicity, fixed-point numbers
are frequently used when hardware cost, speed, and/or
complexity are important issues. Fixed-point places aradix point somewhere in the middle of the digits.
Definition 3 (Fixed-point number) A fixed-point
number a on base b is represented in the form:a  spa1 a2 . . . aip  aip 1 . . . aip f p ,where– sign part sp P t , u determines if a is positive or
negative,– ak P r0, b  1s for each k P r1, ip f ps,– ip is the width of integer part, and– f p is the width of the fraction part.

The set of fixed-point numbers is denoted by Rf x .
We omit the sign if it is positive.
In the fixed-point format pb, ip, f pq,– b is base (e.g. 2 or 10).
– ip is number of digits in the integer part.
– f p is number of digits in the fraction part.
Example 6 The number Π is 3.14159 in the fixed-point
format pb  10, ip  2, f p  5q.
A fixed-point number has a fixed window of representation. The range value that can be represent ispbip  1, bip 1q, and the smallest positive is bf p .

6

2.2.2 OREs of Fixed-point Numbers

2.3 ORE Arithmetic

Roundoff error (RE) If the fraction part of number x(real or floating-point) has more than f p digits, it needs
to truncates to fit the fixed-point format. This loses
information from digits f p 1 in fraction part, and an
RE occurs.

In a program, the propagated error depends on not only
values of variables but also operators of the program.
For instance, the result of fixed-point multiplication
could potentially have as many bits as the sum of thenumber of bits in the two operands. An ORE arithmetic
decomposes a number into a pair of a finite representation and an RE estimation, and each arithmetic operation is defined on such pairs. There are three kinds
of ORE arithmetics corresponding with three kinds of
OREs (e.i., real numbers vs floating-point numbers,
real numbers vs fixed-point numbers, and floating-point
numbers vs fixed-point numbers).

Definition 4 Let x be a real number and let its fixedpoint number representation be xf x under the fixedpoint format pb, ip, f pq. An RE is ref x pxq  x  xf x .
Depending on a rounding mode, the value of RE
may differ. For instance, for a real number x and its
fixed-point representation xf x , the RE ref x pxq satisfies– |ref x pxq|
– |ref x pxq|

2f p for the round toward zero, andbf p {2 for the round to nearest.

Example 7 Let the fixed-point format be pb, ip, f pq 

p10, 8, 7q.

Fixed-point representation x  10{3 is represented as
fixed-point number xf x  3.3333333. The RE is
ref x pxq  xxf x  0.0000000333333333333333333333....
Fixed-point multiplication
4.734612
 5.417242
25.648538980104
25.6485389(after truncating)
It loses information from the 8th digit of the fraction
part 0.000000080104, and its RE is 0.000000080104.

Overflow error (OE) If the integer part of number x(real or floating-point) has more than ip digits before
the radix, it cannot be represented in the fixed-point
numbers, and an OE occurs. More precisely, for a real
number x and fixed-point format pb, ip, f pq, if x ¥ bip ,an OE occurs.
Example 8 For fixed-point format pb  10, ip  8, f p 
7q,4734.612
 54172.42
256485389.80104
Since the integer part has more than 8 digits, an OE
occurs.

2.3.1 Real-to-Fixed ORE Arithmetic
For a real number x and fixed-point format pb, ip, f pq,
we denote the fixed-point part of x by rdf p pxq and
the RE by ref p pxq ( x  rdf p pxq). If rdf p pxq ¡ bip
we conclude that OE occurs, and if ref p pxq ¡ θ (whereθ is predefined threshold) we conclude that RE occurs.
The following definition describes the rules of propagating ORE when converting real numbers to fixed-point
numbers.
Definition 5 (Real-to-Fixed ORE arithmetic)
Let pxf , xr q and pyf , yr q be pairs of fixed-pointparts and REs of real numbers x, y. Real-to-Fixed ORE
arithmetic f  t`, a, b, cu is defined below.
pxf , xr q ` pyf , yr q 
prdf p pxf yf q, xr yr ref p pxf yf qq
pxf , xr q a pyf , yr q 

prdf p pxf  yf q, xr  yr ref p pxf  yf qq
pxf , xr q b pyf , yr q 
prdf p pxf  yf q, xr  yf xf  yr xr  yr ref p pxf  yf qq
pxf , xr q c pyf , yr q 
prdf p pxf  yf q,
pxf xr q  pyf yr q  xf  yf ref p pxf  yf qq

We define the Real-to-fixed ORE comparison operators by comparing the range values of fixed-point
representations. For a given fixed-point representation
pxf , xr q, the corresponding range values are x̃  rxf |xr |, xf |xr |s. The results of Real-to-fixed ORE comparison operators may be true, false, or unknown.
Unknown means that the ranges of a fixed-point expression traverses both true and false of the condition,
and we cannot decide which will hold in real computation. Formally, Real-to-fixed ORE comparison operators are defined as follows:7

Definition 6 (Real-to-fixed ORE comparison operators) Let pxf , xr q, and pyf , yr q be pairs of fixedpoint parts and REs of real numbers x, y.
ppxf , xr q pyf , yr qq $'&true if pxf
false if pxf
'
%

xr yf
xr ¥ yf
unknown otherwise

yr q ^ pxf yf q
yr q ^ pxf ¥ yf q

ppxf , xr q  pyf , yr qq $'&true if pxf  yf ^ xr  yr q
'false if pxf , xr q pyf , yr q _ pyf , yr q pxf , xr q
%unknown otherwise

Other comparison operators, such as ¡, ! , aredefined using the operators above.
Example 9 Let x  34.5678, y  98.76543. We assume
the fixed-point format pb  10, ip  3, f p  2q, “roundtoward 8”, and the RE threshold θ  0.01. We have:– The fixed-point value of x is xf x  34.56 and thecorresponding RE is xr  0.0078– The fixed-point value of y is yf x  98.76 and thecorresponding RE is yr  0.00543
We next show how to evaluate ORE arithmetic:– Addition:

pxf , xr q ` pyf , yr qprdf p p34.56

98.76q, 0.0078
0.00543 ref p p34.56 98.76qq
p133.32, 0.01323q

That means the result of addition is 133.32 and its
RE is 0.01323 ¡ θ. Thus, an RE is detected.
– Multiplication:
pxf , xr q b pyf , yr q 
prdf p p34.56  98.76q, 0.0078  98.76 34.56  0.00543
0.0078  0.00543 ref p p34.56  98.76qq
 p3413.14, 0.963631154q
That means the result of multiplication is 3413.14
p¡ 103 q and its RE is 0.963631154 ¡ θ. Thus, bothan OE and an RE are detected.

Definition 7 (Real-to-Float ORE arithmetic) Let
pxf , xr q and pyf , yr q be pairs of floating-point parts
and REs of real numbers x, y. Real-to-Float ORE arithmetic f  t`, a, b, cu is defined below.
pxf , xr q ` pyf , yr q 
prdf l pxf yf q, xr yr ref l pxf yf qq
pxf , xr q a pyf , yr q 
rdf l pxf  yf q, xr  yr
pxf , xr q b pyf , yr q 

ref l pxf  yf qq

prdf l pxf  yf q, xr  yf xf  yr xr  yr ref l pxf  yf qq
pxf , xr q c pyf , yr q 
prdf l pxf  yf q, pxf xr qpyf yr q xf  yf ref l pxf 
yf qq
Real-to-float ORE comparison operators are definedsimilar Definition 6.
2.3.3 Float-to-Fixed ORE Arithmetic
For a floating-point number x, the floating-point format pb, p, emaxq, and the fixed-point format pb, ip, f pq,
we denote the fixed-point part by rdf x pxq and the
RE by ref f pxq ( ref x pxq  ref l pxq). If rdf x pxq ¡ bip
we conclude that an OE occurs, and if ref x pxq ¡ θ(where θ is predefined threshold) we conclude that an
RE occurs. The following definition describes the rulesof propagating ORE between floating-point numbers
and fixed-point numbers.
Definition 8 (Float-to-Fixed ORE arithmetic) Let

pxf , xr q and pyf , yr q be pairs of fixed-point parts andREs of floating-point numbers x, y. Float-to-Fixed ORE
arithmetic f  t`, a, b, cu is defined below.
pxf , xr q ` pyf , yr q 
prdf x pxf yf q, xr yr ref f pxf yf qq
pxf , xr q a pyf , yr q 

2.3.2 Real-to-Float ORE Arithmetic

prdf x pxf  yf q, xr  yr ref f pxf  yf qq
pxf , xr q b pyf , yr q 
prdf x pxf  yf q, xr  yf xf  yr xr  yr ref f pxf  yf qq
pxf , xr q c pyf , yr q 
prdf x pxf  yf q,
pxf xr q  pyf yr q  xf  yf ref f pxf  yf qq

For a floating-point format pb, p, emaxq and a real number x, we denote the floating-point part by rdf l pxq
and the RE by ref l pxq ( x  rdf l pxq). If rdf l pxq ¡pb  b1p  bemax , we conclude that OE occurs, andif ref l pxq ¡ θ ) where θ is predefined threshold) we
conclude that RE occurs. The following definition describes the rules of propagating ORE when converting
real numbers to floating-point numbers.

Float-to-fixed ORE comparison operators are defined similar Definition 6.
More precise ORE estimation
When we fix the conversion, such as from the floatingpoint IEEE 754 binary64 p2, 53, 1024q to the fixed-point
p2, ip, f pq with size 2 bytes (e.i., ip f p  16) (which
frequently appears in practice), we can obtain better8estimation of OREs. Assume “round to nearest” in Definition 8.
Let δ  ref x px  y q  ref l pxf  yf q where  P
t , , , u. We now find the bound of δ by considering the bound of ref l pxf  yf q and ref x px  y q:

– Floating-point roundoff error rdf l px  y q:
Assume rdf l px  y q  pp1qs  m  be q, we have|ref l px  yq| 253 e {2. Without loss of generality,
we can assume e ¤ ip (otherwise an OE occurs in
the fixed-point operator pxf  yf q). Thus, we have:|ref l px  yq| 253 e {2253 ip {2253 16f p {2pbecause ip
238f p

f p  16q

– Fixed-point roundoff error ref x pxf  yf q:
Because the fixed-point format is unique, the resultsof the addition and the substraction have the sameformat. Thus, ref x pxf  yf q  0 for  P t , u.
For the multiplication, the fraction part of the result
has 2  f p digits. The fraction part is round to f p
digits, and |ref x pxf  yf q| 2f p {2  22f p {2.
For the division, similarly |ref x pxf  yf q| 2f p {2.
Hence, we obtain the Float64-to-Fixed16 ORE
arithmetic by replacing ref f px  y q with δ , where  P
t , , , u and

$
'
|δ |
'
'
'
&

|δ |

'
|δ |
'
'
'
%|δ |

238f p
238f p
2f p1  22f p1
2f p1 238f p

238f p(2)

3 Interval Arithmetics
In order to estimate OREs of arithmetic operations,
there are two known range representations: classical interval [40] and affine interval [54,55]. In this section, we
firstly describe these two methods in detail in Subsections 3.1 and 3.2. Then, inspired by the idea in [21] forunder approximation, we propose an “extended affineinterval” for overapproximation in Subsection 3.3. Lastly,
we represent how to implement these intervals on computers using floating-point type in Subsection 3.4.

Definition 9 A classical interval of x is an intervalx  rxl , xh s with xl ¤ x ¤ xh . The set of classicalintervals is denoted by R.

Definition 10 CI arithmetic consists of operationst ,  ,  , u on pairs of CIs defined below:

rxl , xh s ryl , yh s  rxl yl , xh yh s
rxl , xh s  ryl , yh s  rxl  yh , xh  yl s
rxl , xh s  ryl , yh s  rminpxl yl , xl yh , xh yl , xh yh q,
maxpxl yl , xl yh , xh yl , xh yh qs
rxl , xh s  ryl , yh s  rxl , xh s  r y1 , u1 s if 0 R ryl , yh shl

The following example demonstrates how to compute CI operations:
Example 10 For x P x  r1, 3s, y P y  r6, 10s. Let
us compute the bound of z  x  y ( P t , , , u)using CI:
– Addition z  x
zx

y:

y

 r1, 3s r6, 10s r1  6, 3 10s
 r7, 13s– Substraction z  x  y:zxy
 r1, 3s  r6, 10s r1  10, 3  p6qs
 r11, 9s– Multiplication z  x  y:zxy
 r1, 3s  r6, 10s
 rmint6, 10, 18, 30u, maxt6, 10, 18, 30us
 r18, 30s– Division z  x  y:zxy
 r1, 3s  r6, 10s
Since 0 P r6, 10s, we cannot compute the bound ofz; instead a “devision by zero” warning occurs.

3.1 Classical Interval
Classical interval (CI) was introduced in the 1960s by
Moore [40] as an approach to putting bounds on rounding errors in mathematical computations. In CI, theupper and the lower bounds describe possible values.

For x, x1 , ..., xn P R,  P t , , , u, and a constant c, we denote:– x1 x2  x1  x2 , cx  xc  x  rc, cs,– c°  x  rc, cs  rxs, x  c  x  rc, cs, andn– i1 xi  x1 x2
   xn .

9CI arithmetic assumes that all intervals are independent, even if exact values are dependent. The next
example illustrates such a problem.
Example 11 Let x P x  r1, 3s. It is easy to see that:x  x  r1, 3s  r1, 3s
 r4, 4s

The range of values described an AI is evaluated byreplacing each noise symbol i with r1, 1s.
The advantage of AI is precision on linear operations, compared to CI. For instance, in Example 11,
values in a CI x  r1, 3s are equivalently described by
an AI x:  1 2εx . Then,: xz:  x::0

CI arithmetic assumes the first operand and the second
operand to be independent, while in fact, they represent
the same value x and the exact result is r0, 0s.

which shows the exact result of the subtraction px  xq.

This leads to a great loss of precision in a long computation chain, which is called “error explosion”.

For multiplication, there are choices
approximate°to°nnB, and a direct approximation of B is p i1 |xi |qp i1 |yi |q.
For division, we apply Chebyshev approximation below.
Chebyshev approximation in division
Chebyshev approximation aims to minimize the maximum absolute error. Let F be some space of functions, e.g., polynomials, affine forms. An element of F
that minimizes the maximum absolute difference from agiven function f over a specified domain Ω is known asa Chebyshev (or minimax) F-approximation to f overΩ. We briefly overview the results in [54].
For univariate functions, the minimax affine approximation is characterized by the following property.

3.2 Affine Interval
Affine interval (AI) was introduced by Stolfi [54, 55]
as a model for self-validated numerical analysis. It was
proposed to address the “error explosion” problem inconventional CI. In AI, the value are represented asaffine combinations (affine forms) of certain primitivenoise symbols, which stand for sources of uncertainty
in the data or approximations made during the computation.
Definition 11 An Affine interval of x is a formula:  x0x   xn εnwith x P rx0  i |xi |, x0
i |xi |s. x0 is called thecentral value. For each i P r1, ns, εi P r1, 1s is a noise
°n

x1 ε1

x2 ε2

°n

symbol, which stands for an independent componentof the total uncertainty. The set of affine interval forms:
is denoted by R.
In AI arithmetic, the results of linear operations(e.i., addition, subtraction) are straightforward operations on AIs. However, the results of nonlinear operations (e.i., multiplication, division) are not AI forms.
Hence, we need to approximate the nonlinear parts of
the results by introducing new noise symbols.
Definition 12 AI arithmetic consists of operations: on pairs of AIs as defined below. Lett : , : , °: ,n u°n
:  x0:  y0xi1 xi εi and yi1 yi εi . AI operations

are as defined below:°n: : y:  px0 y0 qx°in1 pxi yi qεi: y:  px0  y0 q:xi1 pxi  yi qεi°n: y:  x0 y0:x
xi y0 qεii1 px0 yi: y:  x: p y1: q, if 0 R rx0 
:
x
:

°n
i

|xi |, x0

Bεn 1

°n
i

|xi |swhere εn 1 P r1, 1s is a new noise symbol, B is the°n°nmaximum value of p i1 xi εi qp i1 yi εi q, and y1: is computed by Chebyshev approximation [54].

Theorem 1 [54] Let f be a bounded and continuousfunction from some closed and bounded interval I 
ra, bs to R. Let h be the affine function that best approximates f in I under the minimax error criterion.
Then, there exist three distinct points u, v, w P I where
the error f pxq hpxq has maximum magnitude; and thesign of the error alternates when the three points are
considered in ascending order.
This theorem provides an algorithm for finding the
optimum approximation in many cases, via the following corollary:
Corollary 1 [54] Let f be a bounded and twice differentiable function defined on some interval I  ra, bs,
whose seconde derivative f 2 does not change sign inside
I. Let f a pxq  αx ζ be its minimax affine approximation in I. Then:– The coefficient α is simply pf pbq  f paqq{pb  aq,
the slope of the line rpxq that interpolates the points
pa, f paqq and pb, f pbqq.
– The maximum absolute error will occur twice (withthe same sign) at the endpoints a and b of the range,and once (with the opposite sign) at every interior
point u of I where f 1 puq  α.
– The independent term ζ is such that αu ζ  pf puq
rpuqq{2, and the maximum absolute error is δ |f puq  rpuq|{2.

10This result gives us a method for finding the optimum
coefficients α and ζ, as long as we can solve the equation
f 1 puq  α.
If an AI y: includes zero, a “division by zero” warning occurs. Thus, we only consider the cases y  rl, hs
are entirely either positive or negative (i.e., l ¡ 0 orh 0). The Chebyshev approximation of y1: (Fig. 4) iscomputed as follows:– a  mint|l|, |h|u, b  maxt|l|, |h|u.
– α  1{b2 .
– dmax  1{a  αa, dmin  1{b  αb.
– ζ  pdmin dmax q{2, if l 0 then ζ  ζ.
– δ  pdmax  dmin q{2.
– y1:  αy: ζ δεk , where εk is a new noise symbol.

– y:  28εy

Let us compute the bound of z  x  y ( P t , u)using AI:
– Addition z  xy:z:  x: : y:
 p1 2εx q : p2
 3 2εx 8εy8εy q

The AI projection of z: is r3  2  8, 3r7, 13s.
– Multiplication z  x  y:

2

8s 

: y:
:
z:  x p1 2εx q : p2 8εy q
 2 4εx 8εy 16ε1

where ε1 is new noise symbol standing for εx εy .
The AI projection of z: is r2  4  8  16, 2 4 8
16s  r26, 30s.
3.3 Extended Affine Interval

a

u

b

Fig. 4 Chebyshev approximation for y1:

Conversion between CI and AI
Standard range representation is CI. To apply AI,
conversion between them are needed.
– CI to AI : Given a CI x  rl, hs, a correspondinghl:  l 2h
AI is x2 εk . Under valuations of noise
symbol εk to r1, 1s, they represent the same range.
This is called AI coercion.
:  x0– AI to CI : An AI x
Σin1 xi εi is projectednto a CI x  rx0  Σi1 |xi |, x0
Σin1 |xi |s.
This projection loses information on dependency ofuncertainty. This is called AI projection.
The following example demonstrates how to propagate the ranges by using AI:
Example 12 For x P x  r1, 3s, y P y  r6, 10s. The
corresponding AI coercions of x, y are:
:1
– x

2εx

AI is more precise than CI for linear operations, buteach time we perform a nonlinear operation, it introduces a new noise symbol. This would be problematicfor a program with a large number of nonlinear operations.
In [21], instead of introducing new noise symbols, coefficients of noise symbols are replaced with CIs. Arithmetic operations are designed for under approximation,
and we apply similar ideas for overapproximation. Thisis called an extended affine interval (EAI), which also
avoids introduction of new noise symbols for nonlinear
operations.
Definition 13 An extended affine interval of x is
a formulap  x0
x
°n

n
¸



xk εk

k 1

with x P x0k1 xk r1, 1s, where εi P r1, 1s is
a noise symbol for each i P r1, ns and xj P R for eachj P r0, ns. The set of extended affine intervals is denotedpby R.
The linear operations of EAI arithmetic are designed
similarly to those of AI arithmetic. For nonlinear operations, unlike AI, EAI arithmetic does not need to
introduce new noise symbols. The results of nonlinear operations approximate nonlinear parts, with CI
coefficients. For example, let us consider°nthe multiplip  x0p
cation of two EAIs. Let xi1 xi εi , y

11

°n



y°0

°
 r s °  r s °p p p  p
q p p
q

° 

p
q

°
°

i 1 y i εi . Without loss of generality, assume thatnny1, 1  k 1 xk 1, 1 . We have:
k 1 k
n
n
x y
x0
y0
i 1 xi εi
i 1 y i εinx0 y 0xi y 0 xi B εi , where B
i 1 x0 y inn1, 1 .
i 1 y i εi . A direct approximation of B is
k 1 yk







r s

Formally, EAI arithmetic is defined as follows:– Addition z  xẑ  x̂ ˆ ŷ
 p1 2εx q ˆ p2
 3 2εx 8εy# °n
p i°1 xi εi qYBnwhere:Xp

i 1 y i εiq

if Y  X
otherwise

and y1p is computed by Chebyshev approximation [54].
Similar to AI arithmetic, the commutative property
holds for both addition and multiplication; the associative property only holds for addition; and the distributive property does not hold.
Remark 2 The overapproximation B may conceal somenoise symbols. If we are sensitive to this matter, B canbe modified as:°nB  αp°nq βX p i1 yi εi qwith α  p|X ||X | |Y |q and β  p1  αq.
i 1 xi εi Y

Conversion between CI and EAI
To apply EAI, the conversion between them areneeded.
– CI to EAI : Given a CI x  rl, hs, a correspondinghl
EAI is x̂  l 2h
2 εk . Under valuations of a noise
symbol εk to r1, 1s, they represent the same range.
This is called EAI coercion.
– EAI to CI : An EAI x̂  x0 Σin1 xi εi is projected
to a CI x  x0
Σin1 xi r1, 1s. Replacement ofa noise symbol εk to r1, 1s loses information on
dependency of uncertainty. This is called EAI projection.
Example 13 For x P x  r1, 3s, y P y  r6, 10s. The
corresponding EAI coercions of x, y are:– x̂  1– ŷ  2

2εx
8εy

8εy q

The EAI projection of ẑ is3

Definition 14 EAI arithmetic consists of operations

t p , p , p , p u on °pairsof EAIs.
°nnxpyp  y 0Letxx0i1 i εi ,°i 1 y i ε i , X °nnk1 pxk r1, 1sq, and Y k1 py k r1, 1sq. Then,°p p yp  px0 y0 q °ni1 pxi yi qεixnp p yp  px0  y0°q
xi1 pxi  y i qεinxp p yp  x0 y0
pxx°Bi y 0 qεii 1 0 y in1ppp  yp  xp  p yp q if 0 R x0xk1 xk r1, 1sy:2r1, 1s8r1, 1s  r7, 13s– Multiplication z  x  y:ˆ ŷẑ  x̂  p1 2εx q ˆ p2
 2 4εx 8εy

8εy q
B

where X  2r1, 1s  r2, 2s and Y  8r1, 1s 
r8, 8s.
Because X  Y . Hence, B  8εy X  r16, 16sεy .
Then, ẑ  2 4εx r8, 24sεy
The EAI projection of ẑ is2

4r1, 1sr8, 24sr1, 1s  r26, 30s

Although EAI does not introduce new noise symbols, this does not mean EAI arithmetic is always lessprecise than AI arithmetic. AI arithmetic only advances
in cases when we reuse the results of nonlinear parts.
Example 14 Let z  x  x; t  z  z and x P r1, 31s.

:  1 2εx , z:  1 4εx 4ε1 where– AI arithmetic: x
ε1 is introduced for multiplication εx εx .
: z:  0
t:  z:p  12εx , zp  1 r0, 8sεx .
– EAI arithmetic: xˆ ẑ  r8, 8sεxt̂  ẑ 

In this case, AI is more precise than EAI. However, if wecompute the bound of t  x  x  x  x (without reusing
the multiplication x  x), both AI and EAI return thesame bound.

3.4 Interval Representations by Floating-point
Numbers
As pointed in [54, 55], the interval representations themselves are affected by OREs, since boundaries and coeffcients are represented by floating-point numbers. We
will briefly overview how to overapproximate CI, AI,
and EAI.
For x P R, we define:– Ó x P Rf l is the round toward 8 of x,– Ò x P Rf l is the round toward 8 of x, and12Floating-point classical interval
For CI, a safe approximation is to truncate down
the lower bound and truncate up the upper bound of
an interval.
Definition 15 A floating-point classical interval of CIx  rl, hs for l, h P R is

The floating-point EAI arithmetic is obtained byreplacing each CI at a coefficeint by the floating-pointCI.
From now on, we will apply floating-point CI, floatingpoint AI, and floating-point EAI, instead of CI, AI, andEAI, respectively.

Ù x Ù rl, hs  rÓ l, Ò hs.

The set of floating-point classical intervals is denotedby Ù R.
The floating-point CI arithmetic is obtained by applying the Ù operator for each operation  P t , , , u.
For Ù x, Ù y P Ù R, we define Ù x  Ù y Ù pÙ x  Ù y q.
Note that, since Ó x ¤ x ¤Ò x, x Ù x, and theextended  gives an overapproximation, i.e., x  y  ÙpÙ x  Ù yq.
This is confirmed by two steps:– For x, y P R, x Ù x and y Ù y. Hence, for  P
t , , , u, px  yq  pÙ x  Ù yq.
– By definition, pÙ x  Ù y q  Ù pÙ x  Ù y q.

Floating-point affine interval
For AI, instead of truncating coefficients in an appropriate way, we simply introduce a new noise symcol.
Definition 16°An Floating-point affine interval ofn::  x0AI x
k1 xk εk P R is a formulaÙ x: Ó x0n¸Ó xk εk

Bεn 1

k 1

where new° noise symbol εn 1 is introduced for REsnand B  k0 pÒ xk  Ó xk q. The set of floating-point:
extended affine intervals is denoted by Ù R.
The floating-point AI arithmetic is obtained by introducing a new noise symbol for each operation°nof AI
arithmetic. For example, let Ù x: Ó x0
k 1 Ó
°nxk εk , Ù y: Ó y0
Ó
y
ε
be
two
floating-point
k k
k 1
AI. The addition isÙ x: Ù y: Ó pÓ x0 Ó y0 qn¸Ó pÓ xk Ó yk qεk Bεn 1

k 1

°n

where B  k 1 pÒ pÓ xk Ó yk q Ó pÓ xk Ó yk qq.
Floating-point extended affine interval
For EAI, we safely approximate CI coefficients by
the floating-point CI.
Definition 17 A floating-point
extended affine in°npp  x0terval of EAI xxεk1 k k P R is

Ù xp Ù x0n¸Ù xk εk .

k 1

The set of floating-point extended affine intervals is dep
noted by Ù R.

4 ORE Analysis as Weighted Model Checking
It has been suggested intimate connections between dataflow
analysis and model checking [41, 50]. A program is firstly
encoded into a model (transition system) by abstraction, and a program analysis is formulated as a model
checking problem. This is nicely adopted for control
flow analysis and/or classical dataflow analysis in Dragonbook [1, 28]. However, as natural requests, we intend
more richer dataflow, such as quantity properties withmore precise treatments on conditional branches. For
instance, linear constraint propagation [41], affine relation analysis [49], or ORE constraint analysis [44]are such examples. In these cases, the direct encoding will be a-transition-as-an-environment-transformer,
which requires all possible environments as states. This
will lead the state explosion problem in model checking.
In 2003, Rep [48] proposed weighted pushdown model
checking, in which each transition is associated with aweight. A weight directly represents dataflow, that is,
how an abstract environment will be transformed, without generating explicit environments as states. This will
not improve complexity in theory, but in practice we
can combine with an on-the-fly generation of weights,
which drastically reduces the search space during model
checking.
We follow this weighted model checking approach(but without using a pushdown stack). Due to infinity (or unboundedness) of weight domains for the ORE
analysis, we restrict ourselves to acyclic models only.
This is a strong limitation, but our main application
target is DSP algorithms, which typically consists ofloops with bounded number of iterations and arrayswith fixed lengths. An effective widening operation design to avoid this restriction is left for future work. We
also put an input range for the ORE analysis, since a
narrower input range results more precise analysis results. As side effect, this also enables us to generateweights in an on-the-fly manner.

13

4.1 Dataflow Analysis as Weighted Model Checking
4.1.1 Weighted Model Checking
Weighted model checking computes dataflow (or, an update of environments) by associating a weight to eachtransition in the model, and the goal is to determine
the weight summary of the meet-over-all-path.

Weighted model checking. Weighted model checking finds
the weight summary of pathspc, c1 q, which is the summation `σPpathspc,c1 q v pσ q.
There are two kinds of generalized reachability problems:Definition 20 Let W  pP, S, f q be a weighted transition system with P  pP, ∆, s0 q. Let C  P andc P P.

– The generalized predecessor problem is to find
1 1
Weight domain and weighted transition system. In weighted δ pcq  `tv pσ q | σ P pathpc, c q, c P C u.
– The generalized successor problem is to findmodel checking, the weight domain D is an idempotent
δ pcq  `tv pσ q | σ P pathpc1 , cq, c1 P C usemiring.
Definition 18 An idempotent semiring is a quintuple pD, `, b, 0, 1q, where 0, 1 P D and `, b are binary
operators on D such that, for a, b, c P D,
– pD, `q is a commutative monoid with the unit 0,– pD, bq is a monoid with the unit 1,– b distributes over `, i.e., a bpb ` cq  pa b bq`pa b cq
and pa ` bq b c  pa b cq ` pb b cq,– ` is idempotent, i.e., a ` a  a, and– 0 is the zero element of b, i.e., a b 0  0 b a  0.

In the context of dataflow analysis, each element of
an idempotent semiring is regarded as follows:

If a cycle exists in a weighted model, pathspc, c1 q becomes infinite. For the termination of a weighted model
checking, an idempotent semiring needs to be bounded.
Definition 21 An idempotent semiring is bounded
if there are no infinite descending chains wrt , wherea  b if, and only if, a ` b  a.
4.2 Weight Domain for ORE Analysis
For an ORE problem, we abstract a concrete environment as an abstract environment by using intervals.

– 0 stands for interruption of dataflow,– 1 stands for the identity function (i.e., no state update),– b is the composition of two successive dataflow, and– ` merges two dataflow at the meet of two transition
sequences.

Definition 22 Let V ar be the set of all variables ofthe program. An abstract environment at a program
location is the set of functions AbsEnv  tV ar Ñ ΦkK u,:K , Φ
pK u. We define
where k  |V ar| and ΦK P tΦK , Φ
the zero environment e0 P AbsEnv by e0 pxq K forx P V ar. Let e, e1 P AbsEnv, and environment meet
operation is defined below:

The weighted transition system is then defined as atransition system “plus” a weight domain.

where \ P t\, \
:,\
p u.

Definition 19 Let P  pP, ∆, s0 q be a transition system with P to be a finite set of states, ∆p P  P q
to be a set of transitions, and s0 pP P q to be an initial state. A weighted transition system (WTS) isa triplet W  pP, S, f q, where S  pD, `, b, 0, 1q is
an idempotent semiring and f : ∆ Ñ D is a map thatassigns a weight to each transition.
Let ∆ be the set of all sequences of transitions.
For σ  rr1 , . . . , rk s P ∆ , we define v pσ q ∆ f pr1 q b. . . b f prk q. If σ is a transition sequence from a statec to a state c1 , we denote c ñσ c1 . The set of all suchsequences is denoted by pathspc, c1 q, i.e.,pathspc, c1 q  tσ | c ñσ c1 ue \ e1  λx.epxq \ e1 pxq

Weight design
The standard definition of a weight domain has thebase set of weights D  AbsEnv Ñ AbsEnv. We thentheoretically define the weight domain for D as follows:
Definition 23 The weight domain (bounded idempotent semiring) S  pD, `, b, 0, 1q withD  AbsEnv Ñ AbsEnv,
1  λx.x,0  λx.e0 ,$'&λx.w1 pxq \ w2 pxq if w1 , w2  0
w1 ` w2  w1
if w2  0'%w
if w1  0
# 2
w2  w1 if w1 , w2  0
w1 b w2 0otherwise

14

where \ P t\, \
:,\
p u.

4.3 ORE Analysis

However, this does not satisfy the descending chain
condition (boundedness), since intervals are infinitely
many (thus the abstract domain is infinite). To copewith this problem, we:– restrict the models to be acyclic,– fix an initial abstract environment I, and– generate weight on-the-fly.
In the context of our ORE analysis, the intuition
behind the first two is,– a target program has bounded loops only; thus after unfolding loops, abstraction produces an acyclic
transition system, and– the result of ORE analysis depends heavily on the
input value; we will set a possible range of inputs at
the program entry in advance.
On-the-fly weight generation
We first introduce the augmented weight domain toassociate an input abstract environment to each weight.
“ ” means any input.
Definition 24 The augmented weight domain S 
pD , `, b, 0 , 1 q consists of D  tpW, wq | W P
AbsEnv, w P Du, 0  p , 0q, 1  p , 1q, and#
pW1 , w1 ` w2 q if W1  W2w `w 
12

w1 b w2 #0pW2 , w1 b w2 q0otherwise
if W1  w2 pW2 q
otherwise

for w1  pW1 , w1 q, w2  pW2 , w2 q P D .
Now we are ready to define the on-the-fly weight domain SP,I for a transition system P and I P AbsEnv.
The intuition is, starting from the initial abstract environment I, only reachable instances of weights arecomputed in on-the-fly manner.

The ORE analysis problem will be solved as weighted
model checking on acyclic models by the following steps(Fig. 5).
1. As preprocessing, translate a C program into CIL(three address code language). Then, each loop are
unfolded and each array is replaced with a set ofvariables (as many as its length). We obtain an
acyclic program without arrays.
2. Generate weighted transition system, which is a control flow graph with an associated ORE arithmetics
operation corresponding to a CIL instruction. ORE
arithmetics is prepared for three types (CI, AI, EAI).
3. Apply weighted model checking. During model checking, weights are generated by an on-the-fly mannerfrom given initial ranges of input parameters.
4.3.1 Abstract domain for ORE problem
Abstract domain
The abstract value of a variable aims to cover allof its possible values at one program location. For theORE problem, the abstract value is a pair of fixed point
and roundoff error ranges. We will show three kinds ofabstractions based on CI, AI, and EAI range representations.
Definition 26 Let f xp and rdf be corresponding range
representations of fixed point and roundoff error.
CI abstract domain Φ  tpf xp, rdf q|f xp, rdf P Ru
:  tpf xp, rdf q|f xp, rdf P R:uAI abstract domain Φppu
EAI abstract domain Φ  tpf xp, rdf q|f xp, rdf P R
For a fresh symbol K (which stands for undefined oruninitialized ), we define ΦK  Φ Y tKu.
Abstract arithmetic
Abstract arithmetic aims to propagate both fixed
point ranges and roundoff error ranges of variables.

Definition 27 Replacing pxf , xr q, pyf , yr q, f, and  in
Definition 25 For a transition system P and I P AbsEnv, the definition of ORE arithmetic (Definition 8) withthe weight domain SP,I  pDP,I , `, b, 0, 1q is a sub– pxf , xr q, py f , y r q, f  t`, a, b, cu, and , we obtain
semiring of S  with DP,I  D . DP,I is given by
CI abstract arithmetic,
"
*
1

1
σ
σ1 1
–
px:f , x:r q, py:f , y:r q, f:  t :̀ , a: , b: , c: u, and :, we obtainpW, wq ^Dσ,Wσ Pv∆pσqpDIc,q c^ PwP. vs0pσñ1 q c ñ c
AI abstract arithmetic, and– px
pf , xpr q, pypf , ypr q, fp  t p̀ , ap , bp , cp u, and p, we obtain
EAI abstract arithmetic,
In implementation, we will identify D  AbsEnv  AbsEnv  AbsEnv by
pW, wq  pW, wpW qq
for W P AbsEnv, w P D.
D with D

where#  rbf p {2, bf p {2sp:  pbf p {2qεr with a fresh noise symbol εr

15

C programint main () {fixed x; int n; int i;
rst = x; i = 0;
while (i <= n) {…

3 address codes

C front-end
CIL

int main {fixed x; int n; int i;
rst = x; i = 0;
if (i <= n) {…

Weighted model checking
Transition system + Weight function
1(v_inf, v_ine) ∈ Itv×Itv

2

AbstractT
5

3F
4 (v_outf, v_outr) ∈ Itv×Itv…

ORE abstraction

ORE report
OE may occur for x
RE of x lies within [0,0.0012]…

Model checker
Weighted PDS libraryFig. 5 ORE analysis as weighted model checking

To illustrate how to create EAI abstract numbers andcompute EAI abstract arithmetic, we consider the following example:
Example 15 The EAI abstract numbers px̂f , x̂r q, pŷf , ŷr q
for variables x, y, respectively, in Example 1 are"x
pf  r1, 1s r2, 2sε1
5 5x
" pr  r2 , 2 sε3
ypf  r0, 0s r10, 10sε2
ypr  r25 , 25 sε4Definition 28 Replacing pxf , xr q, pyf , yr q, in the definition of x̃ in ORE comparisons (Definition 6) with
– pxf , xr q, py f , y r q, we obtain CI abstract comparison operations o  t¤, u,:f , x:r q, py:f , y:r q, we obtain AI abstract compar– px:  t¤: , uison operations o: , and– px
pf , xpr q, pypf , ypr q, we obtain EAI abstract comp  t¤p , p u.
parison operations o

The following example illustrates how to evaluatesince f p  5, the REs of x and y are in r2f p1 , 2f p1 s EAIabstract comparison p .
r25 , 25 s p r0.03125, 0.03125sq and δ  26 
211 243  26 .
pf , xpr q, and pypf , ypr q as in Example 17.
Example 16 Use px
Then, at the line 2 (rst  x  x), pry
stf , ry
str q pxpf , xpr q p 0 is evaluated as follows:
pxpf , xpr q bp pxpf , xpr q is projected as follows:– xf  r1, 3sry
stf  xpf p xpf
– xr  r25 , 25 pr1, 1s r2, 2sε1 q p pr1, 1s r2, 2sε1 q
Since pxf , xr q
0 is unknown, we can conclude
 r1, 1s r0, 8sε1that px
pf , xpr q p pypf , ypr q is unknown.
ˆxry
str  2
pf ˆ x̂r p xpr ˆ xpr ˆ δ
 r0.031250, 0.031250s r0.123091, 0.123091sε1 Meet operation
At the meet of two paths in a program, we need
r0.059615, 0.065385sε2
to combine the results that are generated from these
Abstract comparison operations
paths. The result of the meet must bind all input abInstead of nondeterministic transitions at a condistract values. We first consider how to compute thetional branch, the conditional expression can often be
union of two ranges:
evaluated by using abstract environment. This is usefulin avoiding unnecessary execution paths. The abstract
Definition 29 The unions of ranges are:comparison operations are defined by using ORE comparisons as follows:– CI: rx , x sYry , y s  rminpx , y q, maxpx , y qs.
l

h

l

h

l

l

h

h

16

pu0 °ni°1 ui εi q Y: pv0 °ni1 vi εi q  p u 2 v
n|u v | εn 1i1 ti εi q where εn 1 P r1, 1s is a
2

– AI:
0

0

0

0

instruction”x y z”

 

new noise symbol and, for each i,
ti 

#

ui
vi

if |ui | ¡ |vi |,otherwise.

– EAI:
pu 0
pu0 Y v0 q

“if x

°n

°n i1 ui εi q Yp pv0i1 pui Y v i qεi .

°ni 1 v i ε i q  y then s”

Control inst.

maintest{
st1.
if (x > 0) {st2.
rst = x * x;}else {
st3.
__cil_tmp1 = (Real )3;
rst = __cil_tmp1 * x;}st4.
rst -= y;st5.
return (rst);
st6. }

Definition 30 The meets in abstract values are:K \pxf , xr q  pxf , xr q\ K pxf , xr q.

1

Table 2 Weight function of ORE analysis

Then, the result of meet operation is a pair of theunion of fixed point ranges and the union of roundoff
error ranges.
– CI meet: pxf , xr q \ py f , y r q  pxf Y y f , xr Y y r q:f , x:r q \:f Y:r Y– AI meet: px: py:f , y:r q  px
: y:f , x
: y:r qpf , zpr q \p pypf , ypr q  pxpf Yp ypf , xpr Yp ypr q– EAI meet: px\ P t\, \: , \p u is extended to ΦK P tΦK , Φ:K , ΦpK u byweightpWi , txo  yi e zi , vo  vi |v P V arztxuuq
where e is the corresponding
abstract arithmetic operation of 
0 if xi e yi  false; 1 otherwise,
where e is the corresponding
abstract comparison of 

Fig. 6 CIL code for Example 1

4.3.2 Weighted transition system for ORE analysis

st1
if (x>0)In preprocessing phase, C programs are transformed
into CIL, a three address code language. We replaceeach array with fixed length by a set of variables that
correspond to locations in an array. Thus, our target
instructions are restricted as follows.

if not(x>0)

st2

st3

rst = x*x

rst =3*x

st4
rst =rst-y– Assignment: “x  y  z” with  P t , , , {u.
– Conditional instruction: “if x  y then s” wherest5
s is an instruction and  P t , , ¡, ¡, , ! 
return rst
u. If the condition px  yq is false, s is not visited;
otherwise, s is visited.
st6– Control instruction: “return loc”, “goto loc”, “break”,“continue”. Control moves to the specified location,and the values of variables do not change.
Fig. 7 CFG of three address codes in Fig. 6– While Loop: “while x  y { body }” with  P t, , ¡, ¡, , ! u. body is repeated as long as the
Example 17 We use EAI representation type.
condition px  y q holds. Inside body, “break” will exit
The CIL codes of the C program in Fig. 2 are shown
from the loop.
in Fig. 6. Let st1, ..., st6 be its locations.
In preprocessing phase, the bounded while loops are
To distinguish variables at each locations, we will
unfolded as a sequence of conditional instructions, anddenote a variable v at the location sti by v piq . The
we obtain an acyclic CIL program.
piq piq
fixed-point value and RE of v are denoted by v̂f , v̂r
The weight function is defined as follows:
respectively.
The transition system is P  pP, ∆q, where P Definition 31 For an acyclic transition system P andt
st1,
st2..., st6u, ∆ is shown in Fig. 7 and f is defined
I P AbsEnv, the weight function fP,I : ∆ Ñ DP,I is
in
Table
3.
given in Table 2.
The initial abstract environment Winit at st1 is genThen, we obtain the weighted transition system:
erated from initial range values of variables (given in the
topmost comments in Fig. 2), in that:W  pP, S , f q.
P,I

P,I

We explain how to generate a weighted transition
system by Example 1 (in Introduction).

# pinitqx pr1, 1s r2, 2sε1 , r25 , 25 sε3 qy pinitq  pr10, 10sε2 , r25 , 25 sε4 q17Then, the resulting weighted transition system is W , f q.
init

pP, SP,W

transition(st1,st2)(st1,st3)(st2,st4)(st3,st4)(st4,st5)(st5,st6)

weightif xpinitq p 0
f alse 0 else 1
if not xpinitq p 0
f alse 0 else 1

pp

¡ q
q
¡ q
q
pWipinq , trstp2q  xpinq bp xpinq ,v p2q  v pinq | v P V ar ztrstuuq
pW pinq , t cil tmp1p3q  3,
p xpinq ,rstp3q  cil tmp1p3q bv p3q  v pinq | v P V ar zt cil tmp1, rstuuq
pW pinq , trstp4q  rstpinq ap ypinq ,v p4q  v pinq | v P V ar ztrstuuq
pp

RE bound of rst is by r0.279341, 0.279341s by replacing each εi with r1, 1s in r̂.
By nature of analysis, this analysis overapproximatesREs. It occurs at the conditional branch (line 1) and themultiplication. For instance, at st2, δ̂ (in b̂) is approximated with r0.031250, 0.031250s.
The example above shows that the overapproximations will occur at (1) nonlinear operations; (2) undecided conditional branch. In case the conditional branch
is decided, analysis will not overapproximate it. Below,
how the treatment of conditional branches in ORE analysis will improve the overapproximation.

1

Table 3 Weight function for a CIL code in Example 17

Since the abstraction is an overapproximation, we
conclude soundness of ORE analysis.
Theorem 2 An ORE analysis on a subclass of acyclic
CIL programs is sound.
4.3.3 ORE Analysis Example

Example 19 In Example 18, if we reduce the initial
range of xf to r1, 3s, the condition x ¡ 0 is decided
to be true at st1, and CANA ensures that st3 will not
be executed. Then, at st4, by substraction â,
rpr0.031250, 0.031250s r0.123091, 0.123091sε1
r0.059615, 0.065385sε3r0.031250,  0.031250sε4

RE of rst is bounded by r  r0.250976, 0.250976s
by replacing each εi with r1, 1s in r̂.
This result is more precise than that in Example 18.

We continue to explain how ORE analysis works by theexample in Fig. 2.

4.4 Experiments

p1q p1q q and

Implementation

Example 18 Let the input EAI xp1q  px̂f , x̂r

p1q p1q
y p1q  pŷ , ŷr q as shown in Example 17.
f

St1 is a conditional branch. Since the initial range ofx is r1, 3s, CANA cannot decide the condition x ¡ 0.
Thus, it traces both st2 and st3, and later merges theirresults.
At st2, the RE of rst is computed by multiplicationb̂ as:

p2 q

ry
str

r0.031250, 0.031250s r0.123091, 0.123091sε1
r0.059615, 0.065385sε3

and at st3,

p3q

ry
str

 3ˆ x̂r  r0.093750, 0.093750sε3

And they are merged as:ry
str r0.031250, 0.031250s r0.123091, 0.123091sε1
pr0.059615, 0.065385s Y r0.093750, 0.093750sqε3
r0.031250, 0.031250s r0.123091, 0.123091sε1
pr0.059615, 0.093750sqε3
At st4, by subtraction â, we get the RE of rst:

p4q

xr
rst

r0.031250, 0.031250s r0.123091, 0.123091sε1
r0.059615, 0.09375sε3 r0.031250, 0.031250sε4

We have implemented our analysis framework in a tool
C ANAlyzer (CANA). CANA uses two libraries: CIL
library 3 and WPDS library 4 .
– CIL (C Intermediate Language) is a high-level representation that permit source-to-source transformation of C programs. CIL is used to generate threeaddress codes, information about variables, and the
CFG of a C program.
– WPDS (Weighted Pushdown System) is a library,which provides functions to the sets of forward- or
backward- reachable configurations in a weighted
pushdown system. Since we exclude procedure calls
and unbounded loops, we adopt WPDS only forweighted finite acyclic state transition systems
The inputs of CANA are subclass of ANSI C programs and initial ranges of variables. The outputs of
CANA are roundoff error ranges of variables at eachpoint of the program, and warning about overflow errors(if they occur). CANA has six main modules (Fig. 5.4)
as follows:34

http://hal.cs.berkeley.edu/cil/
http://www.fmi.uni-stuttgart.de/szs/tools/wpds/

18[x]
real err
CI
AI
EAI

C program
Input ranges of vars
RE threshold[0,0.2]0.01909
0.04373
0.03770.03232[0.2,0.4]
0.03
0.05990.04060.0356[0.4,0.6]
0.03891
0.09172
0.06179
0.05763[0.6,0.8]
0.061588
0.148848
0.104468
0.100454

CIL library
CANA system

Stm Info

Expression library

Var & Fun Info

CFG

error range

Interval arithmetics

Collect data

Create PDS

Create Fun f

0.16
0.14
0.12
0.1
0.08
0.06
0.04
0.02
0
[0,0.2]

WDomain[0.2,0.4][0.4,0.6]
x range

WPDS[0.6,0.8]

a. The analysis result of P5(x)WPDS library
ORE report[x]real err
CI
AI
EAI

1. Collect data module generates information required
for the analysis, including: statement information(Stm Info), (2) variable and function information(Var and Func Info), and (3) CFG of C program.
2. Range arithmetics module includes three types ofinterval arithmetics: CI arithmetic, AI arithmetic,and EAI arithmetic.
3. Evaluate exps module evaluates the abstract valuesof expressions based on types of range arithmetics.
4. Create PDS module generates transition system fromcontrol flow graph of a C program.
5. Create Fun f module assigns a weight to each transition.
6. WDomain module defines two operations: b and `.

error range

Fig. 8 CANA system[0,0.2]0.006470.02040.02035
0.01759[0.2,0.4]
0.01080.02080.02040.0176[0.4,0.6]
0.01049
0.021390.020290.01749[0.6,0.8]
0.010206
0.022198
0.019976
0.017184

0.16
0.14
0.12
0.1
0.08
0.06
0.04
0.02
0
[0,0.2][0.2,0.4][0.4,0.6]
x range[0.6,0.8]

b. The analysis result of Sin(x)[exps]
real err
CI
AI
EAI[0,30]
1.36309
1.73766
1.634531.63453[30,60]1.36311.73771.63451.6345[60,90]1.36309
1.73766
1.634531.63453[90,120]
1.363086
1.737656
1.634531
1.634531

2

We have implemented in CANA three types of interval
representations: CI, AI, and EAI. CANA can analyze
programs that have nested loops 64  64.
In order to compare the efficiency of EAI arithmetic
to CI and AI arithmetics, we analyzed source codes ofthree examples:
1. a program computes a polynomial of degree 5
2. a program computes the sine function
3. a tiny fragment, which frequently appears in the
mpeg decoder reference algorithm.
Fig. 9 shows experimental results of analyzing these
programs (on PC with Intel(R) Core(TM) Duo CPU

error range of exp_acc

Experimental results

1.8
1.6
1.4
1.2
1
0.8
0.6
0.4
0.2
0
[0,30][30,60][60,90]exps range
Test

CI

AI

c. The analysis result of pMpeg(exps)
Fig. 9 The experimental results[90,120]EAI

191.66GHz, 1.5Gb of memory). Fig. 9a shows results ofanalyzing the program that computes P 5pxq  1  x
3x2  2x3 x4  5x5 , where the fraction part f p  8. The
true err row is the width of roundoff error ranges which
are found by testing; the CI, AI, and EAI rows are thewidths of roundoff error ranges computed by CI arithmetic, AI arithmetic, and EAI arithmetic, respectively.
Our experiments show that EAI is more precise thanCI and is comparable to AI. We got similar results forthe program that computes sine of x shown in Fig. 9b,
and the fragment of the mpeg decoder pM peg pexpsq in
Fig. 9c. All tests run in less than 2 seconds.

5 Detecting REs based on
Counterexample-guided Narrowing
Static analysis is useful in proving safety properties
of ORE problem. But it requires overapproximationin both propagating REs and control flows like conditional branches. Hence, it may return spurious counterexamples. Fortunately, in our setting, the floating to
fixed-point conversion, we can compute the exact RE,
whereas there are in general no ways to compute exact
real numbers. Though testing can return exact REs, itcannot cover all possible inputs. If we are lucky, witness of large REs would be eventually found, yet mostof them may be missed. Another challenging problem
is how to reduce the number of test cases if the input
domain is large and the input parameters are many.
A popular approach to deal with spurious counterexamples is counterexample-guided abstraction refinement (CEGAR) [6]. Inspired by CEGAR, we combine
testing and RE analysis.
This section proposes an approach for detecting REs
of C programs, which combines static analysis and testing, and make them refine each other. We call this combination counterexample-guided narrowing. First, we apply an overflow and roundoff errors analysis from ourprevious work [44] which returns an overapproximationof REs as an Extended affine interval (EAI). Fortunately, an EAI represents the relations between the input value and the RE of the output. These relations
can be used to clarify: variables are irrelevant to REs
of the results, variables affect the REs the most, and theranges of inputs are most likely to cause the maximum
RE. These observations effectively narrow the focus of
test data generation. Second, in case testing does notfind a witness of RE violation, the analysis may overapproximate too much. Further, the narrower the input ranges are, the more precise the analysis result will
be. Therefore, with a “divide and conquer” refinement
strategy, we can check the most suspicious part first.

Throughout the section, we focus only on roundoff
errors. We assume that ORE analyzer (CANA) does
not detect any overflow errors.

5.1 Observation on RE Analysis
The inputs of an RE analysis consist of– a C program (with m-input variables) to be analyzed (base b  2),– a fixed-point format psp, ip, f pq,– an RE threshold θp¡ 0q, and– a pair of a fixed-point range rli , hi s and an RE range
rlm i , hm i s with 2f p1 lm i ¤ hm i 2f p1
for each i-th input variable.
We will fix the last three elements as an environmentof the RE analysis. We call the Cartesian product D 
rl1 , h1 s      rl2m , h2m s an input domain.
Throughout the RE analysis, all ranges are represented as EAIs with 2m noise symbols (where εi andεm i correspond to noise symbols of the fixed-pointpart and the RE of values of the i-th input variable).
Thus, we coerce input CIs to EAIs by EAI coercion. In
the context of the RE analysis, we denote:
Input domain D  rl1 , h1 s  rl2m , h2m s is pv̂1 , . . . , v̂2m qli
with v̂i  p li 2hi q p hi 2 qεi .
As notational convention, the analysis result is denoted by an EAI:
rp  r0°2m


i 1 r i εiThe analysis result r̂ shows extra information about
the effects of inputs on r̂, since EAI coercions of input
ranges and r̂ share common noise symbols. If violations
are found (i.e., EAI projection of r̂ exceeds rθ, θs),
we need to check whether they are spurious by testing.
Fortunately, we have useful observations below, which
will optimize test data generation and testing.
– RE bound for each test case: Assume that thevaluation of noise symbols for the test case t 
pt1 , . . . , t2m q is pλ1 , . . . , λ2m q, i.e.,
λi 

#

0

if li  hi

pli hi q otherwise
phi li q2tiThen, the RE for the input t is bounded by thevaluation of r̂ with pλ1 , . . . , λ2m q.
– Irrelevant noise symbol: If the coefficient of anoise symbol εk is rk  r0, 0s, the noise symbol εkwill not affect the RE of result.
– Sensitivity of noise symbols: If |rk | ¤ |rh |, thenoise symbol εk affects r̂ more than εh .

20

The following example will demonstrate how theyaffect the testing phases:
Example 20 In the analysis result of Example 18:– For the test case t  pxf , yf , xr , yr q  p1, 5, 0, 0q,
the valuation of noise symbols is pε1 , ε2 , ε3 , ε4 q 
p0, 0.5, 0, 0q. The RE bound of t isr0.031250, 0.031250s  r0.26, 0.26s
Therefore, t is not a counterexample.
– Since r2  r0, 0s, ε2 is an irrelevant noise symbol.
Hence, v2 (or fixed-point part of y) does not affect
RE of rst.
– We have |r1 |  0.123091  maxt|r1 |, . . . , |r4 |u, thus
ε1 is the most sensitive noise symbol. Hence, v1 (orfixed-point part of x) affect the RE of rst the most.
The analysis result is helpful to optimize test phase,includes:– Pre-evaluate test case: if RE bound of a test caset lies in the RE threshold bound, we need not execute test for t.
– Reduce input ranges: which reduces segmentsin each input range if corresponding REs are subsumed. Especially, for an irrelevant noise symbol.
– Choice of the number of ticks, which takes more
ticks in the input ranges of more sensitive noise symbols.

5.2 Refining Test Data Generation
5.2.1 Test Data Generation
For an input domain D  rl1 , h1 s      rl2m , h2m s, abasic strategy of test data generation is to divide theinput domain into meshes and select one test case fromeach mesh.
Definition 32 For an interval rl, hs, and k ¡ 1, the kticks of rl, hs starting from c are tc, c ∆,    , c pk 
1q∆u where ∆  hkl and c is a number lies in rl, l ∆s.
Remark 3 This c intends a randomly generated flicker;
since refinement loops will repeat, we would like to
avoid generating the same test cases.
Example 21 Let us consider the C program as Fig. 2.
– For xf P r1, 3s, let k1  10, then ∆1  p3 
p1qq{10  0.4. Let c1  0.8, we got the set ofticks Xf  t0.8,  0.4, , 3.8u
– For xr P r25 , 25 s, let k2  10, then ∆2  p25 p25 qq{10  0.00625. Let c2  0.03, we got theset of ticks Xr  t0.03,  0.02375, , 0.0265u– For yf P r10, 10s, let k3  10, then ∆3  p10 
p10qq{10  2. Let c3  9, we got the set of ticks
Yf  t9,  7, , 9u– For yr P r25 , 25 s, let k4  10, then ∆4  p25 p25 qq{10  0.00625. Let c4  0.028, we got theset of ticks Yr  t0.028,  0.02175, , 0.0285u
Hence, the set of test data is T  Xf  Yf  Xr  Yr .
E.g., For test case t1  p0.8, 9, 0.03, 0.028q, theinput of fixed-point program is px, y q  p0.8, 9q; theinput of floating-point program is px, y q  p0.83, 9.028.
For an input domain D  rl1 , h1 s      rl2m , h2m s,
all combinations of ki -ticks of rli , hi s for i ¤ 2m are
the set of test data. Then, we execute a program in two
ways: with floating-point arithmetic and fixed-point arithmetic. The difference between them is a true RE. However, the number of test data grows with the power ofthe 2m-th degree.
5.2.2 Range Reduction
For two ranges rl1 , h1 s, rl2 , h2 s, we denote rl1 , h1 s ¤rl2 , h2 s if u ¤ v for each u P rl1 , h1 s and v P rl2 , h2 s(i.e., h1 ¤ l2 ). Reducing input range is executed basedon the observation as the following lemma.
Lemma 2 Assume 0 R ru, v s. Then,– rv, us ¤ ru, v sr uv , uv s ¤ ru, v s if 0 u ¤ v– ru, v s ¤ ru, v sr uv , uv s ¤ rv, us if u ¤ v 0This lemma means that if 0 R rui , vi s  ri we canignore test data with corresponding noise symbol εi inr uvii , uvii s (resp. r uvii , uvii s) for 0 ui ¤ vi (resp. ui ¤vi 0). The reason for this is that the true REs for test
data with εi in r uvii , uvii s (resp. r uvii , uvii s) are boundedby the valuations when a noise symbol εi is either 1 or
1 whatever a true coefficient has a value in rui , vi s.
In a special case ui  vi  0, a valuation of εi does
not matter. Thus, only a valuation with 0 is considered.
From observations above we reduce the input domain D to two input domains Dmax (which contain an
input that causes the maximum RE) and Dmin (whichcontain an input that causes the minimum RE) without loosing opportunities to find test cases that cause
violation of REs.
Definition 33 For an input domainD
p l1 2h1 h1 2l1 ε1 q      p l2m 2h2m h2m 2l2m ε2m q andthe analysis result
rp  ru0 , v0 s

2m
¸



i 1

rui , vi sεi ,21

the subdomain Dmax of D is

p l1 2 h1 h1 2 l1 ε1 q  p l2m 2 h2m h2m 2 l2m ε2m q
where$ |u |'
r |v | , 1s
'
'
'
|v |
&
i

r1,  |u | s
i

εi 

i

'
r0, 0s'''%r1, 1si

if 0

ui ¤ vi

if ui ¤ vi

0

if ui  vi  0otherwise

and the subdomain Dmin is

p l1 2 h1 h1 2 l1 ε1 q  p l2m 2 h2m h2m 2 l2m ε2m q
where

$
'
r1,  ||uv || s'''
& |v |i

if 0

ui ¤ vir |u | , 1s
if ui ¤ vi 0'
r0, 0sif ui  vi  0'''%r1, 1sotherwise°2m
An EAI rp  r0i1 r i εi is maximum (resp. miniεi stronger effect on the RE of the result. For example,
the variable corresponding to dominant noise symbol
will strongly affect REs, in other words, the changing
of this variable causes the changing of RE the most.
Therefore, setting more ticks on the initial range of thisvariables can lead the test cases to various REs. Basedon this observation, our basic idea is, in input domains
Dmin , Dmax , the initial range of variables which are
predicated strongly affect REs will be set more ticks
than other initial ranges. The strategy of setting number of ticks is then depending on coefficients of noise
symbols in analysis result as follows:°2m

Definition 34 Let r̂  r0i0 εi be analysis resultof input domain D1  ru1 , v1 s      ru2m , v2m s.
For σ ¡ 0, a tick frequency ti (wrt σ) for the input
interval rui , vi s isiiimum) if each of elements r0 and ri εi is maximized(resp. minimized). Thus the maximal (resp. minimal)
RE will occur among valuations of εi in ru{v, 1s (resp.
r1, u{vs) if 0 u ¤ v, and in r1, v{us (resp.
rv{u, 1s) if u ¤ v 0. Therefore, from Lemma 2, we
obtain the next theorem.
Theorem 3 If there exists a counterexample in D, thenthere exists a counterexample in Dmax Y Dmin .
Example 22 By observation of analysis result r̂ in Example 18, we can find Dmax of the input domain D
is

ti 

# 2 r |
r|

1

i

σ

s

if ui vi
if ui  vi

Here, rxs denotes the round up of x.
Example 23 For r̂ in Example 18 and Dmax in Example 22, the tick frequency t1 , t2 , t3 , and t4 wrt σ  0.01
(of ε1 , ε2 , ε3 , and ε4 , respectively) are,s  25t1 r 20.123091
0.01
t2 1
t3 r 20.09375
s  190.01
t4 1

Thus, the number of test cases is 25  1  19  1  475,
and the RE found by testing 475 test cases is 0.219720.

5.3 Refinement of Analysis by Narrowing Inputq
pr1, 1s r2, 2sε1 qpr10, 10sε2 qpr25 , 25 sε3 qpr25 , 25 sε4Domains
with ε1  r1, 1s, ε2  r0, 0s, ε3  r0.63589, 1s, andAn analysis may report spurious counterexamples. Forε4  r1, 1s. Hence, Dmax is projected to
tunately, our RE analysis becomes more precise if anr1, 3sr0, 0sr0.019872, 0.03125sr0.03125, 0.03125s. input domain becomes narrower. There are two reasons that make input domain decomposition reduces
Hence, we can conclude that the input with yf  0 andthe overapproximations:yr  0.03125 will cause the maximum RE.
5.2.3 More Ticks for more Sensitive Noise Symbols
We need a strategy to setting ticks for each initial ranges
in input domain. A bad strategy of setting ticks will create several test cases which cause similar REs and all ofthem lie within RE threshold bound. Testing over thesetest cases are not needed.
Analysis result r̂ shows the effects of noise symbols
to the REs. A larger coefficient of a noise symbol causes– a smaller input domain is more likely to be deterministic on conditional branches, and– a smaller input domain is more likely makes EAI
arithmetic more precise.
Our “divide and conquer” strategy has two phases:– Reduce an input domain D to Dmax and Dmin (Definition 33)– Divide the input ranges (in Dmax and Dmin ) of themost sensitive noise symbol εk into two ranges.

22

Definition 35 Let Dmax  rl1 , h1 s  . . .  rl2m , h2m s
be an input domain and εk be the most sensitive noise
symbol. Then:

Not safe!

Dmax

1– Dmax Dmax |v rl , lk hk s

-0.26

0

0.26 rstr

-0.26

0

0.26 rstr

2– Dmax Dmax |v r lk hk ,h s
k
k

k

2

2

k

1
2
where v k is the k-th element of Dmax
(Dmax).
For Dmin , we also have a similar partition strategy.

The next round of the RE analysis will be performed
1
2
for input domains Dmax
and Dmax. Our early experi1
ence shows that often one of analysis results of Dmax
2
and Dmax lie in the RE threshold bound. Thus thissimple strategy becomes quite effective.
Example 24 From Example 20, the most sensitive noise
symbol is ε1 .
Form Example 22, the new input domain Dmax isr1, 3sr0, 0sr0.019872, 0.03125sr0.03125, 0.03125s
and ε1 is the most sensitive symbol (Example 20).
Hence, we will divide the initial range of v1 (r1, 3s)
into two new subranges r1, 1s and r1, 3s and we get:1
Dmax
Dmax |v1 r1,1s
r1, 1s  r0, 0s  r0.019872, 0.03125s
r0.03125, 0.03125s
2
Dmax
Dmax |v1 r1,3s

r1, 3s  r0, 0s  r0.019872, 0.03125s
r0.03125, 0.03125s21reportand Dmax
RE analyses on two domains Dmaxthat:1
– the REs of all input in Dmax
lie in r0.22, 0.22s
2lie in r0.25, 0.25s– the REs of all input in Dmax

Hence, we can conclude the REs of all input in Dmax
lie in RE threshold bound r0.26, 0.26s.
Similarly, we get the REs of all input in Dmin also
lie in the RE threshold bound, and we can conclude theprogram is “safe”. Note that, before decomposition, it
was r0.28, 0.28s (Example 18), which exceeds the RE
threshold bound (Fig. 10). If we reduce RE threshold
1
2
bound θ in 0.219720 θ 0.22, both Dmax
and Dmax
are not enough. In such a case, we will investigate subdomain which has larger RE found testing first in thelater rounds.

D1max

Safe!

2
Dmax

0.26

0

-0.26

rstr

2
1
, DmaxFig. 10 Effects of decomposition of Dmax to Dmax

reduce domain D to Dmin . Function gentestpD, r̂q generate a set of test cases T of domain D using analysis
result r̂. Function testpPf l , Pf x , tq executes both two
programs Pf l , Pf x with test case t and return the difference between result of these two program, called set oftest results DR . Function devidepD, r̂q divides domain
D into two new subdomains D1 , D2 based on analysis
result r̂.
Input: Pf l , Pf x , initial ranges of variables, RE thresholdθOutput: Return “safe” or counterexample or unknown

r s

Initial list of subdomains LD
D , a set of test dataT
, a set of RE DR;
while length LD
10 do
pop one element D from LD ;r̂ analyze Pf l , D ;if r̂θ, θ thencontinue ;endDmax = reduceM ax r̂, D ;Dmin =reduceM in r̂, D ;push Dmin into LD ;rmax max test Pf l , Pf x , t t T ;Let tmax T such that rmax test Pf l , Pf x , tmax ;if rmax θ thenreturn counterexample tmax ;end
D1 , D2
divide Dmax , r̂ ;if tmax D1 thenpush D2 into LD ;push D1 into LD ;elsepush D1 into LD ;push D2 into LD ;end
end
return unknown;

H

H

p q


p
p  r sq

q

p



p

t

t|
P
¡ q

p

u
P

p

p

q

q

q|| P u pqCombining Analysis and Testing Algorithm
Algorithm 5.3 shows the algorithm combining theanalysis and testing. Function analyzepPf l , Dq analyzes
Algorithm 1: Combining analysis and testing
the program Pf l with input domain D, and return theoverapproximate RE in EAI form r̂. Function reduceM axpr̂, Dq
reduce domain D to Dmax . Function reduceM inpr̂, Dqq

23

5.4 Implementation and Experiments

Experimental results

CANAT implementation

Table 4 shows the results of checking 4 programs (onPC with Intel(R) Xeon(TM)CPU 3.60GHz, 3.37Gb ofmemory). The first column shows the names of 4 programs.

C program,Fixed point format,
Input ranges, andRE threshold θ
EAI lib

CIL lib

Convert Fxp

Pflt and
input domain

Pflt and Pfxp

Analysis phase
RE analyzer

Testing phase
Reduce range

Generate test

Subdomain
choiceTest data

DecomposedomainSafe

The best
test case

RE TesterCounterexamples

Fig. 11 CANAT system

Fig. 11 shows the construction of CANAT. CANAT
uses three external tools:– CIL library 5 as a preprocessor,– Weighted PDS library 6 as a backend weighted model
checking engine, and– CANA [44] as an RE analyzer.
CANAT has 4 main modules as follows:
1. Reduce range module clarify: (1) the subdomains of
input domain that contain maximum (or minimum)
REs, (2) the choice of ticks for testing generation.
2. Decompose domain module divides the reduced domain (e.g., Dmax ,Dmin ) into two subdomains.
3. Generate Test module generates set of test data T
based on information obtained from Reduce range
module.
4. RE Tester module automatically generates two programs corresponding to input C program, one uses
fixed-point arithmetic, while the other uses floatingpoint arithmetic. Then, these two programs are executed with the set of test data T . The testing REs
are the differences between the results of these two
programs.
5
6

http://hal.cs.berkeley.edu/cil/
http://www.fmi.uni-stuttgart.de/szs/tools/wpds/

1. P2 from Fig. 1: We set the initial range r1, 3s r10, 10s, f p P t7, 8, 9, 10u, and θ P t0.001 0.002i |0 ¤ i ¤ 9u.
2. P5 that computes P 5pxq  1  x 3x2  2x3 x4 
5x5 : We set the initial range r0, 1s, f p P t7, 8, 9, 10u,and θ P t0.001 0.01i | 0 ¤ i ¤ 9u.
3. Sine that computes the sine function using Taylor
expansion up to degree 21: We set the initial range
r0, 1s, f p P t7, 8, 9, 10u, and θ P t0.001 0.005i | 0 ¤i ¤ 9u.
4. pMpeg that consists of one 8  8 loop taken fromthe mpeg4 decoder reference algorithm: We set theinitial range r0, 30s, f p P t7, 8, 9, 10u, and θ P t0.001
0.05i | 0 ¤ i ¤ 9u.
We compare experimental results by
1. ORE analysis by CANA (CANA) followed by Randomly generated testing (Random test), and
2. Counter example guided narrowing loop by repeating ORE analyes (CANAT anmalysis) and refined
testing (CANAT test).
Both try 40 settings (i.e., different numbers of digits in
fixed-point numbers, different RE thresholds) for eachprogram. For fair comparison, we make the total numbers of test cases to be the same for each setting; Random test generates 200 test cases, and (CANAT test)
generates 20 test cases for each refinement loop, whichis repeated 10 times.
%Checked columns show that how many percentage (among 40 settings) is detected either to be safe or
ORE violation. Although the experiment remains a toy,
it shows clear improvement of testing and analysis.

6 Related WorkThe ORE problems are one of the central issues in the
numerical analysis [17, 13]. There are lots of works onmathemarical reasoning to estimate OREs [17,16], andthere is a well-known methodology for the precise addition of floating numbers, which cancells the effectof REs [27]. It is extended to the precise multiplication [46], and recently verified numerical computation
is evolving.
Our focus is more on static detections of OREs ofprograms, and we omit huge references of these areas,
which are beyond scope of the paper.

24
Input
program
P2
P5
Sine
pMpeg

CANA
15
9
19
11

Random
test
11
15
7
11

Time
(s)
7
14
37
65

%Checked
65.00%
60.00%
65.00%
55.00%

CANAT
analysis
20
12
21
11

CANAT
test
18
19
8
19

CANAT
time(s)
13
24
81
121

%Checkedof CANAT
95.00%
77.50%
72.50%
75.00%

Table 4 Experimental results of CANAT

Range representations of real numbers
Due to REs, we need to evaluate values of real numbers by some representation of ranges. They are classically classified into:– Interval, which is the Cartesian product of one dimensional intervals [2,40].
– Octagon, which is surrounded by either vertical, horizontal, or diagonal lines [39].
– Polyhedra, which is represented as the conjunctionof linear inequalities [8]. Recently, its refinement
SubPolyhedra was proposed [29] by reducing deduction rules among linear inequalities, yet preserving
expressiveness.

technique of [33] is further applied on TMS320 C3X
assembler programs [34].
These ORE analyses are overapproximation, andeasily cause false positives. An ORE analysis with under approximation is proposed based on the mean value
theorem and Kaucher arithmetic [21], to sandwich OREs
from both sides. However, strictly speaking, this underapproximation is for real number variables rather than
floating-point number variables.

– real numbers to floating-point numbers conversion,– real numbers to fixed-point numbers conversion, and– floating-point numbers to fixed-point numbers conversion.

The floating-point numbers to fixed-point numbers
conversion typically appears in hard-wired algorithms
and/or embedded systems. Apart from difficulties in
hardware encoding difficulties [3, 5, 25, 26,37, 51, 52], there
are strong demand to solve ORE problems.
For the floating-point numbers to fixed-point numbers conversion, Fang, et.al. proposed an ORE analysis based on AI, intended for DSP applications [9–11].
We are facing on the same problem, but with different intervals, EAI. In our implementation, we adapted
a sophisticated weighted model checking, whereas they
adapt direct bit-vector encoding. For scalability, theyalso applied probabilistic reduction of the search space.
Thanks to the problem nature, we can examine OREs
by testing, since we can compute both floating-point
numbers and fixed-point numbers. [56] showed a suchtesting tool.
We further combined an ORE analysis and testing by a counter example guided narrowing approach,which refines the focus of testing and avoid false positives in an early stage.
Numerical Constraint Solvers
Recently, several tools have been developed as variations of SMT to solve non-linear numerical constrains.
For instance,

ORE analysis are mainly investigated for the first
and the third.
For the real numbers to floating-point numbers conversion, ORE analysis adapt AI [20,33] (which introduced widening operators to handle loops), except thatthe octagon abstract domain is used in [38].
They are implemented and showed experimental results. FLUCTUAT is presented in [20] and [38] showeda case study on an embedded avionics software. The– iSAT [12], which evaluates non-linear operations tointerval constraints by overfapproximation.
– minismt [57], which covers specific irrationals, suchas rational numbers and roots of small integers. They
are symbolically represented and its bounded searchis encoded as CNF.
– a tool for Simulink/Stateflow models [24], which applied a variation of polyhedra, called the boundedvertex representation for under-approximation.

We are more focus on intervals, and we call a range
described by a pair of the lowest and the highest value
by a classical interval (CI). CI is generalized to allow
swapping of boundaries [18].
By introducing noise symbols, which preserve dependency of uncertainty, Affine interval (AI) has been
proposed [54,55]. Later, we will see how AI is applied
as overapproximation for ORE analyses.
Extended Affine interval (EAI) has proposed for under approximation, based on the mean value theorem
and Kaucher arithmetic [21]. EAI replaces real coefficients of AI with CI coefficients. We apply this idea foroverapproximation of ORE analysis.
ORE analysis
For a static analysis, we need a concrete semantics.
We obey the semantics of propagation of OREs to [32].
There are three kinds of OREs, caused by:

25

Ganai and Ivancic [14] introduced a new method toface with decision problems involving non-linear constraints on bounded integers. Each nonlinear operationis encoded into a Boolean combination of linear arithmetic constraints based on CORDIC algorithm. Then,the linearized formula will be input of a DPLL-style Interval Search Engine that explores various combinationof interval bounds using a SMT solver.
To solve an interval constraint, they divide the input ranges to smaller ranges, which is similar to ours.
Adding to the difference of target domains (i.e., bounded
integers and floating/fixed-point numbers), the differences are, (1) we use EAI instead of CI, (2) combination
with testing, and (3) weighted model checking insteadof (SMT) solver.
To solve dataflow equations over infinite domains,such as numerical constraints (mostly on integers), several algorithms are proposed in the context of weighted
pushdown model checking [19,15,30,41].
The library Apron of numerical abstract domains is
also freely available [23].
Refining analyses and testing
As general setting of static detection, recently therefinement loop of analyses and testing is extensively
investigated.
Counterexample Guided Abstraction-refinement (CEGAR) [6] is widely applied methodology, in which theinitial abstract model typically nondeterministic control structures for conditional branches. When (possible
spurious) counter examples are found, symbolic techniques refine the model by hooking more deterministic
behavior.
Proofs from Tests [4] presented an algorithm DASH
to check if a program satisfies a safety property. It uses
only test generation, and it refines and maintains asound program abstraction as a consequence of failed
test generation operations. This enables us a light-weightrefinement loop with neither any extra theorem provercalls nor any global may-alias information.

and roundoff errors, caused by the floating-point number to fixed-point number conversion. Our contribution
is summarized as follows.
– An extended affine interval (EAI) is newly proposed
to overapproximate overflow and roundoff errors.
EAI has two main advantages over current methods: EAI is more precise than CI and EAI forms are
more compact than AI forms.
– An ORE analysis method based on weighted model
checking is proposed and implemented as CANA.
– The counterexample-guided narrowing, in which ananalysis and testing refine each other, is applied to
the RE problem and implemented as CANAT. Thus,
the result will be more precise than either testing or
static analysis alone.
We also performed preliminary experiments of CANA
and CANAT, which shows optimistic results.
For future works, one obstacle is the scalability of
CANA and CANAT. We are optimistic since DSP algorithms (e.g., digital video compression [47]) are often compositional. They typically consist of sequencesof computations with fixed-length arrays and boundedloops. Therefore, we can divide the algorithm to small
fragments and check each separately.
Second, widening operator design. Currently, we did
not introduce widening operators, but first focus on precision of ORE detection. (For instance, the widening
operator [20] leads to inevitably lose precision a lot.)
Its drawback is that the class of target programs has
strong limitation, though it seems enough for the core
part of DSP encoders/decoders.
We are also interested in an automatic correctionof a program to improve with less OREs. For instance,in [36], there are several techniques to automatically
improve numerical precision, such as:– swapping the order of arithmetic operations,– explicit shifting of the order of magnitude, and– symbolic executions.

Our methodology of counter example guided narrowing tries to refine the focus of testing based on ORE
analysis results. Fortunately, by the nature of EAI, ORE
analysis results tell us which input parameter is dominant for REs. By using this information, we can effectively focus on the most problematic point.

Our ORE analyzer, CANA, can generate the information about range values of fixed-point numbers andtheir RE at each point of the program. There information is helpful information to automatic source code
correction.

7 Conclusion

References

Motivated by automatically detecting OREs of the hardwired conversion of DSP encoders/decoders, this paper
proposed techniques for automatic detection of overflow

1. Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles,Techniques, and Tools. Addison-Wesley (1986)
2. Alefeld, G. and Herzberger, J.: Introduction to Interval Computations. Academic Press, N.Y. (1983)

26
3. Banerjee, P., Bagchi, D., Haldar, M., Nayak, A., Kim, V.,
and Uribe, R.: Automatic Conversion of floating-point MATLAB Programs into fixed-point FPGA Based Hardware Design. In Proc. of the 11th Annual IEEE Symposium on FieldProgrammable Custom Computing Machines, pp. 263, IEEE
Computer Society (2003)
4. Beckman, N.E., Nori, A.V., Rajamani, S.K., Simmons, R.J.,
Tetali, S.D., Thakur, A.V.: Proofs from Tests. In IEEE
Transactions on Software Engineering: Special Issue on the
ISSTA 2008 Best Papers, IEEE Computer Society (2010)
5. Belanovic, P. and Rupp, M.: Automated Floating-Point toFixed-Point Conversion with the Fixify Environment. In
Proc. of the 16th IEEE International Workshop on Rapid
System Prototyping, pp. 172 - 178, IEEE Computer Society(2007)
6. Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H.:
Counterexample-guided abstraction refinement. In Proc. of
the 12th International Conference on Computer Aided Verification , pp. 154-169, Springer-Verlag (2000)
7. Cousot, P. and Cousot, R.: Abstract interpretation: a unified
lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. of the 4th ACM
SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238-252, ACM (1977)
8. Cousot, P. and Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In Proc. of the
5th ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages, pp.84-96, ACM (1978)
9. Fang, C.F., Rutenbar, R.A., and Chen, T.: Fast, accurate
static analyis for fixed-point finite precision effects in DSP
designs. In Proc. of the International Conference on Computer Aided Design, pp. 275-282, IEEE Computer Society(2003)
10. Fang, C.F.: Probabilistic Interval-Valued Computation: Representing and Reasoning about Uncertainty in DSP and VLSI
Design. Ph. D. Diserration, Depterment of Electrical andComputer Engineering, Carnegie Mellon University (2005)
11. Fang, C.F., Rutenbar, R.A., Püschel, M. and Chen, T.: Toward efficient static analysis of finite-precision effects in DSP
applications via Affine arithmetic modeling. In Proc. of Design Automation Conference, pp. 496-501, ACM Press (2003)
12. Franzle, M., Herde, C., Teige, T., Ratschan, S., and Schubert,
T.: Efficient solving of large non-linear arithmetic constraint
systems with complex boolean structure. In Journal on Satisfiability, Boolean Modeling and Computation, Vol 1, pp.
209-236 (2007)
13. Friedman, M. and Kandel, A.: Fundementals of Computer
numerical analysis. CRG Press (1994)
14. Ganai, M.K and Ivancic, F.: Efficient Decision Procedure for
Bounded Integer Non-linear Operations using SMT(LIA),In Proc. of Haifa Verification Conference 2008, LNCS,
vol.5394, pp.68-83, Springer (2009)
15. Gawlitza, T. and Seidl, H.: Precise Fixpoint Computation
Through Strategy Iteration. In Proc. of the European Symposium on Programming 2007,LNCS, vol. 4421, pp. 300315,
Springer (2007)
16. Giraud, L., Langou, J., Rozloznik, M., and Eshof, J.V.D.:
Rounding error analysis of the classical Gram-Schmidt orthogonalization process. Numerische Mathematik, v.101 n.1,
pp.87-100 (2005)
17. Goldberg, D.: What every computer scientist should know
about floating-point arithmetic. ACM Computing Surveys ,pp.5-48, ACM (1991)
18. Goldsztejn, A., Daney, D., Rueher, M., and Taillibert, P.:
Modal intervals revisited: a mean-value extension to generalized intervals, In Proc. of the 1st International Workshop
on Quantification in Constraint Programming, 2005.

19. Gopan, D.: Numeric program analysis techniques with applications to array analysis and library summarization. Ph. D
Thesis, University of Wisconsin-Madison (2007)
20. Goubault, E. and Putot, S.: Static analysis of numerical algorithms. In Proc. of the 13th International Static Analysis
Symposium, pp. 18-34, Springer-Verlag (2006)
21. Goubault, E. and Putot, S.: Under-approximations of computations in real numbers based on generalized affine arithmetic. In Proc. of the 14th International Static Analysis
Symposium, pp. 137-152, Springer-Verlag (2007)
22. 754-2008 IEEE Standard for Floating-Point Arithmetic at:
http://ieeexplore.ieee.org/xpls/abs all.jsp?arnumber=4610935.
Accessed February 2010.
23. Jeannet, B., and Miné, A.: Apron: A library of numericalabstract domains for static analysis. In Proc. of the 21stInternational Conference on Computer Aided Verification,
LNCS, vol.5643, pp. 661-667, Springer-Verlag (2009)
24. Kanade, A., Alur, R., Ivanc, F., Ramesh, S., Sankaranarayanan, S., and Shashidhar, K.C.: Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models. In
Proc. of the 21st International Conference on Computer
Aided Verification, LNCS, vol.5643, pp. 430-445, SpringerVerlag (2009)
25. Keding, H., Hurtgen, F., Willems, M., and Coors, M.: Transformation of Floating-Point into fixed-point Algorithms byInterpolation Applying a Statistical Approach. In Proc. of
the 9th International Conference on Signal Processing Applications and Technology, pp. 270-276, ACM (1998)
26. Kim, S., Kum, K., and Sung, W.: Fixed-point optimization
utility for C and C++ based digital signal processing programs. In IEEE Transactions on Circuits and Systems II,
vol. 45, no.11, pp. 1455-1464, IEEE Computer Society (1998)
27. Knuth, D.E.: The Art of Computer Programming, Vol. 2:
Seminumerical Algorithms. AddisonWesley (2002)
28. Lacey, D., Jones, N.D., Wyk, E.V., and Frederiksen, C.C.:
Proving correctness of compiler optimizations by temporal
logic. POPL, pp.283-294, ACM (2002)
29. Laviron, V. and Logozzo, F.: SubPolyhedra: A (more) scalable approach to infer linear inequalities. Proc. of the 10th
International Conference on Verification, Model Checking,and Abstract Interpretation, LNCS, vol. 5403, pp. 229-244,
Springer-Verlag (2009)
30. Leroux, J. and Sutre, G.: Accelerated data-flow analysis. In
Proc. of the 14th International Static Analysis Symposium,
LNCS, vol. 4634, pp. 184199, Springer (2007)
31. Loh, E. and Walster, G.W.: Rump’s example revisited. Realiable Computing, vol.8 (3), pp.245-248 (2002)
32. Martel, M.: Semantics of roundoff error propagation in finite
precision calculations. In Higher-Order and Symbolic Computation, v19(1), pp.7-30, Springer Netherlands (2006)
33. Martel, M.: Static analysis of the numerical stability of loops.
In Proc. of the 9th International Static Analysis Symposium,
LNCS, vol. 2477, pp. 133-150, Springer-Verlag (2002)
34. Martel, M.: Validation of assembler programs for DSPs:
A static analyzer. In Proc. of ACM SIGPLAN-SIGSOFT
Workshop on Program Analysis for Software Tools and Engineering, pp. 8-13, ACM Press (2004)
35. Martel, M.: Semantics-Based Transformation of Arithmetic
Expressions. In Proc. of the 14th International Static Analysis Symposium, LNCS, vol.4634 pp.298-314, Springer-Verlag(2007)
36. Martel, M.: Program transformation for numerical precision.
In Proc. of ACM SIGPLAN Workshop on Partial Evaluation
and Program Manipulation 2009 pp. 101-109, ACM Press(2009)
37. Menard, D., Chillet, D., Charot, F., and Sentieys, O.: Automatic floating-point to fixed-point conversion for DSP code27
generation. In Proc. of the 2002 international conference on
Compilers, architecture, and synthesis for embedded systems,
pp. 270-276, ACM (2002)
38. Mine, A.: Relational abstract domains for the detection of
floating-point run-time errors. In Proc. of the European Symposium on Programming (ESOP 2004), Vol. 2986, pp. 317,
Springer (2004)
39. Mine, A.: The octagon abstract domain. Higher-Order andSymbolic Computation, Vol.19 (1), pp.31-100, 2006.
40. Moore, R.E.: Interval Analysis. Prentice-Hall (1966)
41. Mller-Olm, M. and Seidl, H.: Precise interprocedural analysis
through linear algebra. In Proc. of the 31st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pp. 330-341, ACM (2004)
42. Necula, G.C., McPeak, S., Rahul, S.P., and Weimer, W.: CIL:
Intermediate Language and Tools for Analysis and Transformation of C Programs. In Proc. of the 11th International Conference on Compiler Construction, pp. 213-228,
Springer-Verlag (2002)
43. Nielson, F., Nielson, H. R., Hankin, C.: Principles of program
analysis. Springer (1998)
44. Ngoc, D.T.B. and Ogawa, M.: Roundoff and Overflow Error Analysis via Model Checking. In Proc. of the 7th International Conference on Software Engineering and Formal
Methods, pp.105-114, IEEE Computer Society (2009)
45. Ngoc, D.T.B. and Ogawa, M.: Checking Roundoff Errors
based on Counterexample-Guided Narrowing. In Proc. of the25th IEEE/ACM International Conference on AutomatedSoftware Engineering, to appear as a short paper (2010)
46. Ogita, T., Rump, S.M., and Oishi, S.: Accurate sum and dot
product. SIAM Sci. Comp, vol.26 (6), pp.1955-1988 (2005)
47. Peter, S.: Digital Video Compression. mcgraw-Hill (2004)
48. Reps, T., Schwoon, S., Jha, S., and Melski D.: Weighted
pushdown systems and their application to interprocedural
dataflow analysis. In Proc. of the 10th International Static
Analysis Symposium, pp. 189-213, Springer-Verlag (2003)
49. Sagiv, M., Reps, T., and Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. In Theoretical Computer Science, v.167 n.1-2, p.131-170(1996)
50. Schmidt, D.A. and Steffen, B.: Program analysis as model
checking of abstract interpretations. In Proc. of the 5th International Conference on Static Analysis Symposium, pp.
351-380, Springe-Verlag (1998)
51. Shi, C. and Brodersen, R.W.: An automated floating-point to
fixed-point conversion methodology. In Proc. IEEE International Conference on Acoust., Speech, and Signal Processing,Vol. 2, pp. 529-532 (2003)
52. Shi, C.: Floating-point to Fixed-point Conversion. Ph. D.
Thesis, University of California - Berkeley (2004)
53. Steffen, B.: Data Flow Analysis as Model Checking. In Proc.
of the International Conference on Theoretical Aspects ofComputer Software, p.346-365, Springer-Verlag (1991)
54. Stolfi, J.: Self-Validated Numerical Methods and Applications. Ph. D. Dissertation, Computer Science Department,
Stanford University (1997)
55. Stolfi, J. and Figueiredo, L.H. de: An introduction to affinearithmetic. In Tendencias em Matematica Aplicada e Computacional, Vol.3(4), pp. 297-312 (2003)
56. Wijaya, S. and Cantoni, A.: A Java Simulation Tool for
Fixed-Point System Design. In Proc. of the 2nd International Conference on Simulation Tools and Techniques, pp.
1-10, ACM (2009)
57. Zankl, H. and Middeldorp, A.: Satisfiability of non-linear(ir)rational arithmetic. In Proc. of the 16th International
Conference on Logic for Programming, Artificial Intelligence, and Reasoning, to appear (2010).