Boosting Verification by Automatic Tuning of Decision Procedures
[PDF] [PS] [PS.BZ2] [VIEW]
Bibtex:
@inproceedings{hbhh07boosting,
author = {Frank Hutter and Domagoj Babi\'c and Holger H.~Hoos
and Alan J.~Hu},
title = {{Boosting Verification by Automatic Tuning of
Decision Procedures}},
year = {2007},
booktitle = {FMCAD'07: Proceedings of the 7th International
Conference Formal Methods in Computer Aided Design},
publisher = {IEEE Computer Society},
address = {Washington, DC, USA},
pages = {27--34},
location = {Austin, Texas, USA}
}
Abstract:
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-theart
SAT solver for large, real-world bounded model-checking
and software verification instances. The resulting, automaticallyderived
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 handtuning
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.