Name
Abstract | ||
|---|---|---|
This paper presents a sound and complete analysis for determining the range of floating-point variables in control software. Existing approaches to bounds analysis either use convex abstract domains and are efficient but imprecise, or use floating-point decision procedures, and are precise but do not scale. We present a new analysis that elevates the architecture of a modern SAT solver to operate over floating-point intervals. In experiments, our analyser is consistently more precise than a state-of-the-art static analyser and significantly outperforms floating-point decision procedures. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-28756-5_5 | tools and algorithms for construction and analysis of systems |
Keywords | Field | DocType |
floating-point variable,floating-point decision procedure,conflict-driven learning,bounds analysis,convex abstract domain,floating-point interval,complete analysis,modern SAT solver,numeric bounds analysis,state-of-the-art static analyser,control software,new analysis | Control software,Analyser,Architecture,Computer science,Abstract interpretation,Boolean satisfiability problem,Algorithm,Regular polygon,Theoretical computer science,Interval arithmetic | Conference |
Volume | ISSN | Citations |
7214 | 0302-9743 | 28 |
PageRank | References | Authors |
0.86 | 23 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Vijay D'Silva | 1 | 239 | 14.07 |
| Leopold Haller | 2 | 127 | 6.93 |
| Daniel Kroening | 3 | 3084 | 187.60 |
| Michael Tautschnig | 4 | 425 | 25.84 |