首页> 外文期刊>Science of Computer Programming >Automatically refining partial specifications for heap-manipulating programs
【24h】

Automatically refining partial specifications for heap-manipulating programs

机译:自动完善堆操作程序的部分规范

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

摘要

Automatically verifying heap-manipulating programs is a challenging task, especially when dealing with complex data structures with strong invariants, such as sorted lists and AVL/red-black trees. The verification process can greatly benefit from human assistance through specification annotations, but this process requires intellectual effort from users and is error-prone. In this paper, we propose a new approach to program verification that allows users to provide only partial specification to methods. Our approach will then refine the given annotation into a more complete specification by discovering missing constraints. The discovered constraints may involve both numerical and multi-set properties that could be later confirmed or revised by users. We further augment our approach by requiring partial specification to be given only for primary methods. Specifications for loops and auxiliary methods can then be systematically discovered by our augmented mechanism, with the help of information propagated from the primary methods. Our work is aimed at verifying beyond shape properties, with the eventual goal of analysing full functional properties for pointer-based data structures. Initial experiments have confirmed that we can automatically refine partial specifications with non-trivial constraints, thus making it easier for users to handle specifications with richer properties.
机译:自动验证堆操作程序是一项艰巨的任务,尤其是在处理具有强不变性的复杂数据结构时,例如排序列表和AVL /红黑树。验证过程可以通过规范注释从人工协助中大大受益,但是此过程需要用户的智力努力,并且容易出错。在本文中,我们提出了一种程序验证的新方法,该方法允许用户仅对方法提供部分说明。然后,我们的方法将通过发现缺失的约束将给定的注释完善为更完整的规范。发现的约束可能涉及数值和多集属性,以后可由用户确认或修改。通过进一步要求仅针对主要方法的部分说明,我们进一步扩展了我们的方法。然后,通过我们的增强机制,可以借助从主要方法传播的信息来系统地发现循环和辅助方法的规范。我们的工作旨在验证超出形状的属性,最终目标是分析基于指针的数据结构的全部功能属性。初步实验证实,我们可以自动优化具有非平凡约束的部分规格,从而使用户更容易处理具有更丰富特性的规格。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号