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, the authors 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.