Boosting Verification by Automatic Tuning of Decision Procedures
Boosting Verification by Automatic Tuning of Decision Procedures
复制标题
DOI：
10.1109/famcad.2007.9
复制
发表时间：
2007-11
期刊：
影响因子：
--
通讯作者：
F. Hutter;Domagoj Babic;H. Hoos;Alan J. Hu
中科院分区：
文献类型：
--
作者：
F. Hutter;Domagoj Babic;H. Hoos;Alan J. Hu
参数化启发式算法在计算机辅助设计和验证中比比皆是，手动调整各个参数是困难和耗时的。人工智能(AI)社区的最新结果表明，此调优过程可以自动化，这样做可以显著提高性能；此外，自动化的参数优化可以在启发式算法的开发过程中提供有价值的指导。在本文中，我们研究了这种人工智能方法如何改进用于大型、真实世界有界模型检测和软件验证实例的最先进的SAT求解器。由此产生的自动派生的参数设置在有界模型检查实例上产生的运行时间平均快4.5倍，在软件验证问题上比广泛的手动调整决策过程快500倍。此外，自动调优的可用性影响了求解器的设计，自动派生的参数设置提供了对问题实例属性的更深层次的了解。
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.