• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Software engineering and formal methods >Counterexamples from Proof Failures in SPARK
【24h】

Counterexamples from Proof Failures in SPARK

机译：SPARK证明失败的反例

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

A major issue in the activity of deductive program verification is the understanding of the reason why a proof fails. To help the user understand the problem and decide what needs to be fixed in the code or the specification, it is essential to provide means to investigate such a failure. We present our approach for the design and the implementation of counterexample generation within the SPARK 2014 environment, exhibiting values for the variables of the program where a given part of the specification fails to be validated. To produce a counterexample, we exploit the ability of SMT solvers to propose, when a proof of a formula is not found, a counter-model. Turning such a counter-model into a counterexample for the initial program is not trivial because of the many transformations leading from a given code and specification to a verification condition.
机译：演绎程序验证活动中的一个主要问题是对证明失败的原因的理解。为了帮助用户理解问题并确定需要在代码或规范中解决的问题，必须提供调查此类故障的方法。我们介绍了在SPARK 2014环境中设计和实施反例生成的方法，并展示了程序变量的值，其中规范的给定部分未能通过验证。为了产生一个反例，我们利用SMT求解器的能力，在找不到公式证明的情况下，提出反模型。由于从给定的代码和规范到验证条件的许多转换，将这样的反模型转换为初始程序的反例并非易事。

著录项

  • 来源
  • 会议地点 Vienna(AU)
  • 作者

    David Hauzar; Claude Marche; Yannick Moy;

  • 作者单位

    Inria, Universite Paris-Saclay, 91893 Palaiseau, France,LRI, CNRS Univ. Paris-Sud, 91405 Orsay, France,AdaCore, 75009 Paris, France;

    Inria, Universite Paris-Saclay, 91893 Palaiseau, France,LRI, CNRS Univ. Paris-Sud, 91405 Orsay, France;

    AdaCore, 75009 Paris, France;

  • 会议组织
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号