Numeric Bounds Analysis with Conflict−Driven Learning
Vijay D'Silva‚ Leopold Haller‚ Daniel Kroening and Michael Tautschnig
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.
Details
| Book Title |
TACAS |
| Year |
2012 |
Links
Related pages
|
People |
Vijay D'Silva | Leopold Haller | Daniel Kroening | Michael Tautschnig |