Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY
Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY
复制标题
了解演绎验证的参数：KeY 的实证研究
DOI：
10.1007/978-3-319-94821-8_20
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
I. Schaefer
中科院分区：
文献类型：
--
作者：
A. Knüppel;T. Thüm;C. Pardylla;I. Schaefer
由于软件系统的正式验证是一项复杂的任务，包括许多算法和启发式，现代定理证明器提供了许多参数，供用户选择以控制如何验证软件。显然，参数的数量甚至随着每个新版本的发布而增加。一个挑战是默认参数通常不足以自动关闭证明，并且在验证工作方面不是最佳的。非专家很难进入验证阶段，他们通常必须遵循耗时的试错策略，为甚至微不足道的软件部分选择正确的参数。为了帮助演绎验证的用户，我们应用机器学习技术来实证研究哪些参数及其组合会损害或提高可证明性和验证工作。我们在演绎验证系统KeY 2.6.1和指定的OpenJDK摘录上举例说明了我们的过程，并提出了53个假设，其中只有3个被拒绝。我们确定了代表高可证明性和低验证努力之间的权衡的参数，使得为任何一个方向优先选择参数成为可能。我们的见解使工具构建者更好地理解了他们的控制参数，并为自动演绎验证和非专家验证工具的更好适用性奠定了基础。
As formal verification of software systems is a complex task comprising many algorithms and heuristics, modern theorem provers offer numerous parameters that are to be selected by a user to control how a piece of software is verified. Evidently, the number of parameters even increases with each new release. One challenge is that default parameters are often insufficient to close proofs automatically and are not optimal in terms of verification effort. The verification phase becomes hardly accessible for non-experts, who typically must follow a time-consuming trial-and-error strategy to choose the right parameters for even trivial pieces of software. To aid users of deductive verification, we apply machine learning techniques to empirically investigate which parameters and combinations thereof impair or improve provability and verification effort. We exemplify our procedure on the deductive verification system KeY 2.6.1 and specified extracts of OpenJDK, and formulate 53 hypotheses of which only three have been rejected. We identified parameters that represent a trade-off between high provability and low verification effort, enabling the possibility to prioritize the selection of a parameter for either direction. Our insights give tool builders a better understanding of their control parameters and constitute a stepping stone towards automated deductive verification and better applicability of verification tools for non-experts.
登录
查看更多内容
携带证明的应用程序：基于合同的部署时验证
DOI：
10.1007/978-3-319-47166-2_58
发表时间：
2016
期刊：
影响因子：
--
作者：
S. Holthusen;M. Nieke;T. Thüm;I. Schaefer
通讯作者：
I. Schaefer
技术转让软件工具手稿编号（将由编辑插入）使用可扩展软件模型检查框架检查 JML 规范⋆
DOI：
10.1007/s10009-005-0218-5
发表时间：
2006
影响因子：
1.5
作者：
N. Polikarpova;Julian Tschannen;Carlo A. Furia
通讯作者：
Carlo A. Furia
形式化方法及其在关键系统认证中的作用
DOI：
10.1007/978-1-4471-0921-1_1
发表时间：
1997
期刊：
2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops
影响因子：
--
作者：
J. Rushby
通讯作者：
J. Rushby
遗留代码的演绎验证
影响因子：
1
作者：
Bernhard Beckert;Thorsten Bormer;Daniel Grahl
通讯作者：
Daniel Grahl
使用 SPL Conqueror 优化模板代码的性能
DOI：
--
发表时间：
2014
期刊：
影响因子：
--
作者：
A. Grebhahn;Norbert Siegmund;S. Apel;S. Kuckuk;Christian Schmitt;H. Köstler
通讯作者：
H. Köstler