Boosting Verification by Automatic Tuning of Decision Procedures

Frank Hutter, Domagoj Babic, Holger H. Hoos, and Alan J. Hu

Formal Methods in Computer-Aided Design (FMCAD), 2007.

Parameterized heuristics abound in computer aided design and
verification, and manual tuning of the respective parameters is
difficult and time-consuming. Very recent results from the artificial
intelligence (AI) community suggest that this tuning process can be
automated, and that doing so can lead to significant performance
improvements; furthermore, automated parameter optimization can provide
valuable guidance during the development of heuristic algorithms.  In
this paper, we study how such an AI approach can improve a
state-of-the-art SAT solver for large, real-world bounded
model-checking and software verification instances.  The resulting,
automatically-derived parameter settings yielded runtimes on average
4.5 times faster on bounded model checking instances and 500 times
faster on software verification problems than extensive hand-tuning of
the decision procedure.  Furthermore, the availability of automatic
tuning influenced the design of the solver, and the
automatically-derived parameter settings provided a deeper insight into
the properties of problem instances.