Name
Abstract | ||
|---|---|---|
This paper proposes a framework for statically analyzing overflow and roundoff errors of C programs. First, a new range representation, ``extended affine interval'', is proposed to estimate overflow and roundoff errors. Second, the overflow and roundoff error analysis problem is encoded as a weighted model checking problem. To avoid widening, currently we focus on programs with bounded loops, which typically appear in encoder/decoder reference algorithms. Last, we implement the proposed framework as a static analysis tool CANA. Experimental results on small programs show that the extended affine interval is much more precise than classical interval. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1109/SEFM.2009.33 | Hanoi |
Keywords | Field | DocType |
separation logic,classical interval,proposed framework,bounded loop,weighted model checking problem,roundoff error analysis problem,pointer program verification,c program,statically analyzing overflow,static analysis tool,extended affine interval,roundoff error,reactive power,resource management,encoding,peano arithmetic,data mining,completeness theorem,formal logic,construction industry,informatics,computer languages | Predicate transformer semantics,Pointer (computer programming),Separation logic,Programming language,Gödel's completeness theorem,Computer science,Assertion,Theoretical computer science,Predicate (grammar),Soundness,Completeness (statistics) | Conference |
ISBN | Citations | PageRank |
978-0-7695-3870-9 | 3 | 0.39 |
References | Authors | |
11 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Makoto Tatsuta | 1 | 111 | 22.36 |
| Wei-Ngan Chin | 2 | 868 | 63.37 |
| Mahmudul Faisal Al Ameen | 3 | 3 | 1.06 |