首页> 外文期刊>Science of Computer Programming >Generating property-directed potential invariants by quantifier elimination in a k-induction-based framework
【24h】

Generating property-directed potential invariants by quantifier elimination in a k-induction-based framework

机译:在基于k归纳的框架中通过量词消除生成属性导向的潜在不变量

获取原文
获取原文并翻译 | 示例

摘要

This paper addresses the issue of potential invariant generation in the formal analysis of transition systems with k-induction, in the linear real/integer arithmetic fragment. First, quantifier elimination is used to find parameters for generic templates such that the said templates become inductive. Second, a backward analysis, also using quantifier elimination, outputs preimages of the negation of the proof objective, viewed as unauthorized states, or gray states. Two heuristics are proposed to take advantage of this source of information and generate potential invariants: a thorough exploration of the possible partitionings of the gray state space, and an inexact exploration regrouping and over-approximating disjoint areas of the gray state space. Both aim at discovering hidden relations between state variables. K-induction is used to isolate actual invariants and to check if they make the proof objective inductive. These heuristics can be used on the first preimage of the backward exploration, and each time a new one is output, refining the information on the gray states. We show, on examples of interest in the application field of critical embedded systems, that our approach is able to prove properties for which other academic or commercial tools fail. The different methods are introduced as components of a collaborative formal verification framework based on k-induction and are motivated through two examples, one of which was provided by Rockwell Collins.
机译:本文在线性实/整数算术片段中,用k-归纳法转换系统形式化分析时,解决了潜在不变性产生的问题。首先,使用量词消除来找到通用模板的参数,以使所述模板成为归纳的。其次,也使用量词消除的向后分析输出证明目标否定的原像,被视为未授权状态或灰色状态。提出了两种启发式方法,以利用这一信息源并产生潜在的不变性:对灰色状态空间可能的分区进行彻底的探索,以及对灰色状态空间的不相交区域进行过度精确的重组和过度逼近。两者都旨在发现状态变量之间的隐藏关系。 K归纳法用于隔离实际不变量,并检查它们是否使证明客观归纳。这些启发式方法可用于向后探索的第一个原像,并且每次输出新的启发式信息时,都会精炼有关灰色状态的信息。我们在关键嵌入式系统的应用领域中感兴趣的示例中表明,我们的方法能够证明其他学术或商业工具无法实现的性能。引入了不同的方法作为基于k归纳法的协作形式验证框架的组成部分,并通过两个示例来激发这些示例,其中一个示例是由Rockwell Collins提供的。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号