Boosting Verification by Automatic Tuning of Decision Procedures Export

@inproceedings{citeulike:6057267, 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-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.}, address = {Washington, DC, USA}, author = {Hutter, Frank and Babi\'{c}, Domagoj and Hoos, Holger H. and Hu, Alan J.}, booktitle = {Proceedings of Formal Methods in Computer Aided Design (FMCAD '07)}, citeulike-article-id = {6057267}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1333874.1334161}, citeulike-linkout-1 = {http://dx.doi.org/10.1109/FMCAD.2007.13}, doi = {10.1109/FMCAD.2007.13}, isbn = {0-7695-3023-0}, keywords = {parameter\_adjustment, satisfiability}, pages = {27--34}, posted-at = {2009-11-02 19:11:31}, priority = {2}, publisher = {IEEE Computer Society}, title = {{Boosting Verification by Automatic Tuning of Decision Procedures}}, url = {http://dx.doi.org/10.1109/FMCAD.2007.13}, year = {2007} }

TY - CONF ID - citeulike:6057267 L3 - citeulike-article-id:6057267 N2 - 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. SN - 0-7695-3023-0 AD - Washington, DC, USA EP - 34 TI - {Boosting Verification by Automatic Tuning of Decision Procedures} PB - IEEE Computer Society T2 - Proceedings of Formal Methods in Computer Aided Design (FMCAD '07) SP - 27 KW - parameter_adjustment KW - satisfiability AU - Hutter, Frank AU - Babić, Domagoj AU - Hoos, Holger AU - Hu, Alan PY - 2007/// UR - http://dx.doi.org/10.1109/FMCAD.2007.13 ER -