Conference item
Numeric bounds analysis with conflict-driven learning
- 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.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Accepted manuscript, pdf, 412.6KB, Terms of use)
-
- Publisher copy:
- 10.1007/978-3-642-28756-5_5
Authors
- Publisher:
- Springer
- Host title:
- TACAS 2012: Tools and Algorithms for the Construction and Analysis of Systems
- Volume:
- 7214
- Pages:
- 48-63
- Publication date:
- 2012-04-09
- DOI:
- ISBN:
- 9783642287565
- Keywords:
- UUID:
-
uuid:530e2d36-b4e4-47cf-8b00-07bda7d45219
- Local pid:
-
cs:5832
- Deposit date:
-
2015-03-31
Terms of use
- Copyright holder:
- Springer-Verlag Berlin Heidelberg
- Copyright date:
- 2012
- Notes:
- © Springer-Verlag Berlin Heidelberg 2012. This is the accepted manuscript version of the article. The final version is available online from Springer at: https://doi.org/10.1007/978-3-642-28756-5_5
If you are the owner of this record, you can report an update to it here: Report update to this record