Numeric Bounds Analysis with Conflict-Driven Learning

Abstract

We present 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.

Documents

• TACAS paper

Experimental Results

For our experiments we used an Intel 64bit system running Fedora 13 Linux. We do expect, however, that the experiments are reproducible on any Linux system.

Our experiments were performed using the CPROVER Benchmarking Toolkit. To repeat our experiments, download cdfpl.tar.gz and cdfpl.cprover-bm.tar.gz and proceed as described on the CPROVER Benchmarking Toolkit's web page.

For reference, all our log files and detailed results are available online as well.

• Benchmark results for Astree
• Benchmark results for CBMC
• Benchmark results for Conflict-Driven Learning, default options
• Benchmark results for Conflict-Driven Learning, without learning
• Benchmark results for Conflict-Driven Learning, range-based decisions

People

Contact Vijay D'Silva, Leopold Haller, Daniel Kroening, Michael Tautschnig with any questions.