预测用于软件验证的SMT求解器性能
软件工程
2017-01-31 v1 机器学习
计算机科学中的逻辑
摘要
Why3 IDE 与验证系统通过基于驱动程序的架构促进了广泛的可满足性模理论（SMT）求解器的使用。我们提出 Where4：一种基于组合的方法来解脱 Why3 证明义务。我们对源自程序源代码的静态度量使用数据分析和机器学习技术。我们的方法通过提供单一工具将证明义务委托给最有可能返回有用结果的求解器，从而使软件工程师受益。它使用现有的 Why3 和求解器安装以时间高效的方式做到这一点——无需用户具备关于 SMT 求解器操作的底层知识。
引用
@article{arxiv.1701.08466,
title = {Predicting SMT Solver Performance for Software Verification},
author = {Andrew Healy and Rosemary Monahan and James F. Power},
journal= {arXiv preprint arXiv:1701.08466},
year = {2017}
}
备注
In Proceedings F-IDE 2016, arXiv:1701.07925