Boosting Verification by Automatic Tuning of Decision Procedures

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 pa...

• Type: Conference
• Year: 2007
• Where: FMCAD
• Authors: Frank Hutter, Domagoj Babic, Holger H. Hoos, Alan J. Hu
• Keywords: FMCAD 2007, Formal Methods, Parameter Settings, Software Verification, Software Verification Instances