Boosting Verification by Automatic Tuning of Decision Procedures

[PDF] [PS] [PS.BZ2] [VIEW]

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